Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-sep | Unicode version |
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
condition replaced by a disjoint
variable condition 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 2959. In some texts, this scheme is called "Aussonderung" or the Subset Axiom. (Contributed by NM, 11-Sep-2006.) |
Ref | Expression |
---|---|
ax-sep |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . . . 5 | |
2 | vy | . . . . 5 | |
3 | 1, 2 | wel 2147 | . . . 4 |
4 | vz | . . . . . 6 | |
5 | 1, 4 | wel 2147 | . . . . 5 |
6 | wph | . . . . 5 | |
7 | 5, 6 | wa 104 | . . . 4 |
8 | 3, 7 | wb 105 | . . 3 |
9 | 8, 1 | wal 1351 | . 2 |
10 | 9, 2 | wex 1490 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: axsep2 4117 zfauscl 4118 bm1.3ii 4119 a9evsep 4120 axnul 4123 nalset 4128 |
Copyright terms: Public domain | W3C validator |