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

Axiom ax-sep 3848
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 2739. 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 1376 . . . 4 wff x y
4 vz . . . . . 6 setvar z
51, 4wel 1376 . . . . 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 1226 . 2 wff x(x y ↔ (x z φ))
109, 2wex 1363 1 wff yx(x y ↔ (x z φ))
Colors of variables: wff set class
This axiom is referenced by:  axsep2  3849  zfauscl  3850  bm1.3ii  3851  a9evsep  3852  axnul  3855  nalset  3860
  Copyright terms: Public domain W3C validator