Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-setind | Unicode version |
Description: Axiom of -Induction (also known as
set induction). An axiom of
Intuitionistic Zermelo-Fraenkel set theory. Axiom 9 of [Crosilla] p.
"Axioms of CZF and IZF". This replaces the Axiom of
Foundation (also
called Regularity) from Zermelo-Fraenkel set theory.
For more on axioms which might be adopted which are incompatible with this axiom (that is, Non-wellfounded Set Theory but in the absence of excluded middle), see Chapter 20 of [AczelRathjen], p. 183. (Contributed by Jim Kingdon, 19-Oct-2018.) |
Ref | Expression |
---|---|
ax-setind |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . . . . 6 | |
2 | va | . . . . . 6 | |
3 | vy | . . . . . 6 | |
4 | 1, 2, 3 | wsb 1749 | . . . . 5 |
5 | 2 | cv 1341 | . . . . 5 |
6 | 4, 3, 5 | wral 2442 | . . . 4 |
7 | 6, 1 | wi 4 | . . 3 |
8 | 7, 2 | wal 1340 | . 2 |
9 | 1, 2 | wal 1340 | . 2 |
10 | 8, 9 | wi 4 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: setindel 4512 elirr 4515 en2lp 4528 zfregfr 4548 tfi 4556 setindft 13740 setindis 13742 |
Copyright terms: Public domain | W3C validator |