Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-bdsep Structured version   GIF version

Axiom ax-bdsep 9339
 Description: Axiom scheme of bounded (or restricted, or Δ0) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 3866. (Contributed by BJ, 5-Oct-2019.)
Hypothesis
Ref Expression
ax-bdsep.1 BOUNDED φ
Assertion
Ref Expression
ax-bdsep 𝑎𝑏x(x 𝑏 ↔ (x 𝑎 φ))
Distinct variable groups:   𝑎,𝑏,x   φ,𝑎,𝑏
Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Axiom ax-bdsep
StepHypRef Expression
1 vx . . . . . 6 setvar x
2 vb . . . . . 6 setvar 𝑏
31, 2wel 1391 . . . . 5 wff x 𝑏
4 va . . . . . . 7 setvar 𝑎
51, 4wel 1391 . . . . . 6 wff x 𝑎
6 wph . . . . . 6 wff φ
75, 6wa 97 . . . . 5 wff (x 𝑎 φ)
83, 7wb 98 . . . 4 wff (x 𝑏 ↔ (x 𝑎 φ))
98, 1wal 1240 . . 3 wff x(x 𝑏 ↔ (x 𝑎 φ))
109, 2wex 1378 . 2 wff 𝑏x(x 𝑏 ↔ (x 𝑎 φ))
1110, 4wal 1240 1 wff 𝑎𝑏x(x 𝑏 ↔ (x 𝑎 φ))
 Colors of variables: wff set class This axiom is referenced by:  bdsep1  9340
 Copyright terms: Public domain W3C validator