Axiom ax-inf2 15622

Description: Another axiom of infinity in a constructive setting (see ax-infvn 15587). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-inf2	|- E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Axiom ax-inf2

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar x
2		va	. . . . 5 setvar a
3	1, 2	wel 2168	. . . 4 wff x e. a
4	1	cv 1363	. . . . . 6 class x
5		c0 3450	. . . . . 6 class (/)
6	4, 5	wceq 1364	. . . . 5 wff x = (/)
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1363	. . . . . . . 8 class y
9	8	csuc 4400	. . . . . . 7 class suc y
10	4, 9	wceq 1364	. . . . . 6 wff x = suc y
11	2	cv 1363	. . . . . 6 class a
12	10, 7, 11	wrex 2476	. . . . 5 wff E. y e. a x = suc y
13	6, 12	wo 709	. . . 4 wff ( x = (/) \/ E. y e. a x = suc y )
14	3, 13	wb 105	. . 3 wff ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
15	14, 1	wal 1362	. 2 wff A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
16	15, 2	wex 1506	1 wff E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )

This axiom is referenced by:  bj-omex2  15623  bj-nn0sucALT  15624