ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-sep Structured version   Unicode 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  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 2757. 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 1391 . . . 4
4 vz . . . . . 6  setvar
51, 4wel 1391 . . . . 5
6 wph . . . . 5
75, 6wa 97 . . . 4
83, 7wb 98 . . 3
98, 1wal 1240 . 2
109, 2wex 1378 1
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