Axiom ax-sep 3638

Description: The Axiom of Separation of ZF set theory. See axsep 3637 for more information. It was derived as axsep 3637 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.

Assertion

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

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

Detailed syntax breakdown of Axiom ax-sep

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 1614	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 1614	. . . . 5 class y
5	2, 4	wcel 1617	. . . 4 wff x e. y
6		vz	. . . . . . 7 set z
7	6	cv 1614	. . . . . 6 class z
8	2, 7	wcel 1617	. . . . 5 wff x e. z
9		wph	. . . . 5 wff ph
10	8, 9	wa 433	. . . 4 wff (x e. z /\ ph)
11	5, 10	wb 231	. . 3 wff (x e. y <-> (x e. z /\ ph))
12	11, 1	wal 1613	. 2 wff A.x(x e. y <-> (x e. z /\ ph))
13	12, 3	wex 1644	1 wff E.yA.x(x e. y <-> (x e. z /\ ph))

This axiom is referenced by:  axsep2 3639  zfauscl 3640  bm1.3ii 3641  axnul 3644

Copyright terms: Public domain