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 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 2785. 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 1410 | . . . 4 |
4 | vz | . . . . . 6 | |
5 | 1, 4 | wel 1410 | . . . . 5 |
6 | wph | . . . . 5 | |
7 | 5, 6 | wa 101 | . . . 4 |
8 | 3, 7 | wb 102 | . . 3 |
9 | 8, 1 | wal 1257 | . 2 |
10 | 9, 2 | wex 1397 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: axsep2 3903 zfauscl 3904 bm1.3ii 3905 a9evsep 3906 axnul 3909 nalset 3914 |
Copyright terms: Public domain | W3C validator |