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

Axiom ax-iinf 4254
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 3218 . . . 4  (/)
2 vx . . . . 5  setvar
32cv 1241 . . . 4
41, 3wcel 1390 . . 3  (/)
5 vy . . . . . 6  setvar
65, 2wel 1391 . . . . 5
75cv 1241 . . . . . . 7
87csuc 4068 . . . . . 6  suc
98, 3wcel 1390 . . . . 5  suc
106, 9wi 4 . . . 4  suc
1110, 5wal 1240 . . 3  suc
124, 11wa 97 . 2  (/)  suc
1312, 2wex 1378 1  (/)  suc
Colors of variables: wff set class
This axiom is referenced by:  zfinf2  4255
  Copyright terms: Public domain W3C validator