Axiom ax-sep 2703

Description: The Axiom of Separation of ZF set theory. It was derived as axsep 2702 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 955	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 955	. . . . 5 class y
5	2, 4	wcel 958	. . . 4 wff x e. y
6		vz	. . . . . . 7 set z
7	6	cv 955	. . . . . 6 class z
8	2, 7	wcel 958	. . . . 5 wff x e. z
9		wph	. . . . 5 wff ph
10	8, 9	wa 223	. . . 4 wff (x e. z /\ ph)
11	5, 10	wb 146	. . 3 wff (x e. y <-> (x e. z /\ ph))
12	11, 1	wal 954	. 2 wff A.x(x e. y <-> (x e. z /\ ph))
13	12, 3	wex 980	1 wff E.yA.x(x e. y <-> (x e. z /\ ph))

This axiom is referenced by:  axsep2 2704  zfauscl 2705  bm1.3ii 2706  axnul 2709

Copyright terms: Public domain