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

Axiom ax-iinf 4472
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 3333 . . . 4 class
2 vx . . . . 5 setvar 𝑥
32cv 1315 . . . 4 class 𝑥
41, 3wcel 1465 . . 3 wff ∅ ∈ 𝑥
5 vy . . . . . 6 setvar 𝑦
65, 2wel 1466 . . . . 5 wff 𝑦𝑥
75cv 1315 . . . . . . 7 class 𝑦
87csuc 4257 . . . . . 6 class suc 𝑦
98, 3wcel 1465 . . . . 5 wff suc 𝑦𝑥
106, 9wi 4 . . . 4 wff (𝑦𝑥 → suc 𝑦𝑥)
1110, 5wal 1314 . . 3 wff 𝑦(𝑦𝑥 → suc 𝑦𝑥)
124, 11wa 103 . 2 wff (∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
1312, 2wex 1453 1 wff 𝑥(∅ ∈ 𝑥 ∧ ∀𝑦(𝑦𝑥 → suc 𝑦𝑥))
Colors of variables: wff set class
This axiom is referenced by:  zfinf2  4473
  Copyright terms: Public domain W3C validator