Axiom ax-sep 4247

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 disjoint variable condition 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 3050. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

The variable x can occur in the formula ph, which in textbooks is often written ph ( x ). To specify this in the Metamath language, we omit the distinct variable condition ($d) that x not occur in ph.

For a version using a class variable, see sepg 4249, which requires the axiom of extensionality as well as the axiom scheme of separation for its derivation.

If we omit the requirement that y not occur in ph, we can derive a contradiction (the ax-sep in set.mm). (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 2210	. . . 4 wff x e. y
4		vz	. . . . . 6 setvar z
5	1, 4	wel 2210	. . . . 5 wff x e. z
6		wph	. . . . 5 wff ph
7	5, 6	wa 104	. . . 4 wff ( x e. z /\ ph )
8	3, 7	wb 105	. . 3 wff ( x e. y <-> ( x e. z /\ ph ) )
9	8, 1	wal 1400	. 2 wff A. x ( x e. y <-> ( x e. z /\ ph ) )
10	9, 2	wex 1545	1 wff E. y A. x ( x e. y <-> ( x e. z /\ ph ) )

This axiom is referenced by:  axsepg  4248  sepg  4249  zfausclOLD  4251  bm1.3ii  4252  a9evsep  4253  axnul  4256  nalset  4261