Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-sep GIF version

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 yx(x y ↔ (x z φ))
Distinct variable groups:   x,y,z   φ,y,z
Allowed substitution hint:   φ(x)

Detailed syntax breakdown of Axiom ax-sep
StepHypRef Expression
1 vx . . . . 5 setvar x
2 vy . . . . 5 setvar y
31, 2wel 1391 . . . 4 wff x y
4 vz . . . . . 6 setvar z
51, 4wel 1391 . . . . 5 wff x z
6 wph . . . . 5 wff φ
75, 6wa 97 . . . 4 wff (x z φ)
83, 7wb 98 . . 3 wff (x y ↔ (x z φ))
98, 1wal 1240 . 2 wff x(x y ↔ (x z φ))
109, 2wex 1378 1 wff yx(x y ↔ (x z φ))
 Colors of variables: wff set class This axiom is referenced by:  axsep2  3867  zfauscl  3868  bm1.3ii  3869  a9evsep  3870  axnul  3873  nalset  3878
 Copyright terms: Public domain W3C validator