Axiom ax-sep 4006

Description: The Axiom of Separation of IZF set theory. Axiom 6 of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed, and with a F/ y ph condition replaced by a distinct variable constraint between y and ph).

The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x e. z) so that it asserts the existence of a collection only if it is smaller than some other collection z that already exists. This prevents Russell's paradox ru 2877. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

(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 1464	. . . 4 wff x e. y
4		vz	. . . . . 6 setvar z
5	1, 4	wel 1464	. . . . 5 wff x e. z
6		wph	. . . . 5 wff ph
7	5, 6	wa 103	. . . 4 wff ( x e. z /\ ph )
8	3, 7	wb 104	. . 3 wff ( x e. y <-> ( x e. z /\ ph ) )
9	8, 1	wal 1312	. 2 wff A. x ( x e. y <-> ( x e. z /\ ph ) )
10	9, 2	wex 1451	1 wff E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

This axiom is referenced by:  axsep2  4007  zfauscl  4008  bm1.3ii  4009  a9evsep  4010  axnul  4013  nalset  4018