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	⊢ ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x))

Distinct variable group:   x,y

Detailed syntax breakdown of Axiom ax-iinf

Step	Hyp	Ref	Expression
1		c0 3218	. . . 4 class ∅
2		vx	. . . . 5 setvar x
3	2	cv 1241	. . . 4 class x
4	1, 3	wcel 1390	. . 3 wff ∅ ∈ x
5		vy	. . . . . 6 setvar y
6	5, 2	wel 1391	. . . . 5 wff y ∈ x
7	5	cv 1241	. . . . . . 7 class y
8	7	csuc 4068	. . . . . 6 class suc y
9	8, 3	wcel 1390	. . . . 5 wff suc y ∈ x
10	6, 9	wi 4	. . . 4 wff (y ∈ x → suc y ∈ x)
11	10, 5	wal 1240	. . 3 wff ∀y(y ∈ x → suc y ∈ x)
12	4, 11	wa 97	. 2 wff (∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x))
13	12, 2	wex 1378	1 wff ∃x(∅ ∈ x ∧ ∀y(y ∈ x → suc y ∈ x))

This axiom is referenced by:  zfinf2  4255