Axiom ax-sep 4781

Description: The Axiom of Separation of ZF set theory. See axsep 4780 for more information. It was derived as axsep 4780 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 11-Sep-2006.)

Assertion

Ref	Expression
ax-sep	|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

Distinct variable groups:   x, y, z   ph, y, z

Allowed substitution hint:   ph( x)

Detailed syntax breakdown of Axiom ax-sep

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar x
2		vy	. . . . 5 setvar y
3	1, 2	wel 1991	. . . 4 wff x e. y
4		vz	. . . . . 6 setvar z
5	1, 4	wel 1991	. . . . 5 wff x e. z
6		wph	. . . . 5 wff ph
7	5, 6	wa 384	. . . 4 wff ( x e. z /\ ph )
8	3, 7	wb 196	. . 3 wff ( x e. y <-> ( x e. z /\ ph ) )
9	8, 1	wal 1481	. 2 wff A. x ( x e. y <-> ( x e. z /\ ph ) )
10	9, 2	wex 1704	1 wff E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

This axiom is referenced by:  axsep2  4782  zfauscl  4783  bm1.3ii  4784  ax6vsep  4785  axnul  4788  nalset  4795  bj-nalset  32794  bj-axsep2  32921