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 2881. 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 1466 | . . . 4 |
4 | vz | . . . . . 6 | |
5 | 1, 4 | wel 1466 | . . . . 5 |
6 | wph | . . . . 5 | |
7 | 5, 6 | wa 103 | . . . 4 |
8 | 3, 7 | wb 104 | . . 3 |
9 | 8, 1 | wal 1314 | . 2 |
10 | 9, 2 | wex 1453 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: axsep2 4017 zfauscl 4018 bm1.3ii 4019 a9evsep 4020 axnul 4023 nalset 4028 |
Copyright terms: Public domain | W3C validator |