Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-iinf GIF version

Axiom ax-iinf 4470
 Description: Axiom of Infinity. Axiom 5 of [Crosilla] p. "Axioms of CZF and IZF". (Contributed by Jim Kingdon, 16-Nov-2018.)
Assertion
Ref Expression
ax-iinf 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-iinf
StepHypRef Expression
1 c0 3331 . . . 4 class
2 vx . . . . 5 setvar 𝑥
32cv 1313 . . . 4 class 𝑥
41, 3wcel 1463 . . 3 wff ∅ ∈ 𝑥
5 vy . . . . . 6 setvar 𝑦
65, 2wel 1464 . . . . 5 wff 𝑦𝑥
75cv 1313 . . . . . . 7 class 𝑦
87csuc 4255 . . . . . 6 class suc 𝑦
98, 3wcel 1463 . . . . 5 wff suc 𝑦𝑥
106, 9wi 4 . . . 4 wff (𝑦𝑥 → suc 𝑦𝑥)
1110, 5wal 1312 . . 3 wff 𝑦(𝑦𝑥 → suc 𝑦𝑥)
124, 11wa 103 . 2 wff (∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
1312, 2wex 1451 1 wff 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
 Colors of variables: wff set class This axiom is referenced by:  zfinf2  4471
 Copyright terms: Public domain W3C validator