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

Axiom ax-sep 3849
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/ condition replaced by a distinct variable constraint between and ).

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

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

Assertion
Ref Expression
ax-sep
Distinct variable groups:   ,,   ,,
Allowed substitution hint:   ()

Detailed syntax breakdown of Axiom ax-sep
StepHypRef Expression
1 vx . . . . 5  setvar
2 vy . . . . 5  setvar
31, 2wel 1375 . . . 4
4 vz . . . . . 6  setvar
51, 4wel 1375 . . . . 5
6 wph . . . . 5
75, 6wa 97 . . . 4
83, 7wb 98 . . 3
98, 1wal 1226 . 2
109, 2wex 1362 1
Colors of variables: wff set class
This axiom is referenced by:  axsep2  3850  zfauscl  3851  bm1.3ii  3852  a9evsep  3853  axnul  3856  nalset  3861
  Copyright terms: Public domain W3C validator