Axiom ax-bdsep 16910

Description: Axiom scheme of bounded (or restricted, or Δ₀) 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 4249. (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

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 setvar x
2		vb	. . . . . 6 setvar b
3	1, 2	wel 2210	. . . . 5 wff x e. b
4		va	. . . . . . 7 setvar a
5	1, 4	wel 2210	. . . . . 6 wff x e. a
6		wph	. . . . . 6 wff ph
7	5, 6	wa 104	. . . . 5 wff ( x e. a /\ ph )
8	3, 7	wb 105	. . . 4 wff ( x e. b <-> ( x e. a /\ ph ) )
9	8, 1	wal 1400	. . 3 wff A. x ( x e. b <-> ( x e. a /\ ph ) )
10	9, 2	wex 1545	. 2 wff E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
11	10, 4	wal 1400	1 wff A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )

This axiom is used by:  bdsep1  16911