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

Axiom ax-bdsep 13009
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 4016. (Contributed by BJ, 5-Oct-2019.)
Hypothesis
Ref Expression
ax-bdsep.1  |- BOUNDED  ph
Assertion
Ref Expression
ax-bdsep  |-  A. a E. b A. x ( x  e.  b  <->  ( x  e.  a  /\  ph )
)
Distinct variable groups:    a, b, x    ph, a, b
Allowed substitution hint:    ph( x)

Detailed syntax breakdown of Axiom ax-bdsep
StepHypRef Expression
1 vx . . . . . 6  setvar  x
2 vb . . . . . 6  setvar  b
31, 2wel 1466 . . . . 5  wff  x  e.  b
4 va . . . . . . 7  setvar  a
51, 4wel 1466 . . . . . 6  wff  x  e.  a
6 wph . . . . . 6  wff  ph
75, 6wa 103 . . . . 5  wff  ( x  e.  a  /\  ph )
83, 7wb 104 . . . 4  wff  ( x  e.  b  <->  ( x  e.  a  /\  ph )
)
98, 1wal 1314 . . 3  wff  A. x
( x  e.  b  <-> 
( x  e.  a  /\  ph ) )
109, 2wex 1453 . 2  wff  E. b A. x ( x  e.  b  <->  ( x  e.  a  /\  ph )
)
1110, 4wal 1314 1  wff  A. a E. b A. x ( x  e.  b  <->  ( x  e.  a  /\  ph )
)
Colors of variables: wff set class
This axiom is referenced by:  bdsep1  13010
  Copyright terms: Public domain W3C validator