Axiom ax-sep 3866

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 Ⅎyφ condition replaced by a distinct variable constraint between y and φ).

The Separation Scheme is a weak form of Frege's Axiom of Comprehension, conditioning it (with x ∈ 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 2757. In some texts, this scheme is called "Aussonderung" or the Subset Axiom.

(Contributed by NM, 11-Sep-2006.)

Assertion

Ref	Expression
ax-sep	⊢ ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ))

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

Allowed substitution hint:   φ(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 1391	. . . 4 wff x ∈ y
4		vz	. . . . . 6 setvar z
5	1, 4	wel 1391	. . . . 5 wff x ∈ z
6		wph	. . . . 5 wff φ
7	5, 6	wa 97	. . . 4 wff (x ∈ z ∧ φ)
8	3, 7	wb 98	. . 3 wff (x ∈ y ↔ (x ∈ z ∧ φ))
9	8, 1	wal 1240	. 2 wff ∀x(x ∈ y ↔ (x ∈ z ∧ φ))
10	9, 2	wex 1378	1 wff ∃y∀x(x ∈ y ↔ (x ∈ z ∧ φ))

This axiom is referenced by:  axsep2  3867  zfauscl  3868  bm1.3ii  3869  a9evsep  3870  axnul  3873  nalset  3878