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

Axiom ax-bdsep 13096
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 4046. (Contributed by BJ, 5-Oct-2019.)
Hypothesis
Ref Expression
ax-bdsep.1 BOUNDED 𝜑
Assertion
Ref Expression
ax-bdsep 𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
Distinct variable groups:   𝑎,𝑏,𝑥   𝜑,𝑎,𝑏
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Axiom ax-bdsep
StepHypRef Expression
1 vx . . . . . 6 setvar 𝑥
2 vb . . . . . 6 setvar 𝑏
31, 2wel 1481 . . . . 5 wff 𝑥𝑏
4 va . . . . . . 7 setvar 𝑎
51, 4wel 1481 . . . . . 6 wff 𝑥𝑎
6 wph . . . . . 6 wff 𝜑
75, 6wa 103 . . . . 5 wff (𝑥𝑎𝜑)
83, 7wb 104 . . . 4 wff (𝑥𝑏 ↔ (𝑥𝑎𝜑))
98, 1wal 1329 . . 3 wff 𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
109, 2wex 1468 . 2 wff 𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
1110, 4wal 1329 1 wff 𝑎𝑏𝑥(𝑥𝑏 ↔ (𝑥𝑎𝜑))
Colors of variables: wff set class
This axiom is referenced by:  bdsep1  13097
  Copyright terms: Public domain W3C validator