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 2763. 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 1394 | . . . 4 |
4 | vz | . . . . . 6 | |
5 | 1, 4 | wel 1394 | . . . . 5 |
6 | wph | . . . . 5 | |
7 | 5, 6 | wa 97 | . . . 4 |
8 | 3, 7 | wb 98 | . . 3 |
9 | 8, 1 | wal 1241 | . 2 |
10 | 9, 2 | wex 1381 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: axsep2 3876 zfauscl 3877 bm1.3ii 3878 a9evsep 3879 axnul 3882 nalset 3887 |
Copyright terms: Public domain | W3C validator |