Axiom ax-sep 2708

Description: The Axiom of Separation of ZF set theory. It was derived as axsep 2707 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 957	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 957	. . . . 5 class y
5	2, 4	wcel 960	. . . 4 wff x e. y
6		vz	. . . . . . 7 set z
7	6	cv 957	. . . . . 6 class z
8	2, 7	wcel 960	. . . . 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 956	. 2 wff A.x(x e. y <-> (x e. z /\ ph))
13	12, 3	wex 982	1 wff E.yA.x(x e. y <-> (x e. z /\ ph))

This axiom is referenced by:  axsep2 2709  zfauscl 2710  bm1.3ii 2711  axnul 2714

Copyright terms: Public domain