Axiom ax-inf2 13858

Description: Another axiom of infinity in a constructive setting (see ax-infvn 13823). (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 2137	. . . 4 wff x e. a
4	1	cv 1342	. . . . . 6 class x
5		c0 3409	. . . . . 6 class (/)
6	4, 5	wceq 1343	. . . . 5 wff x = (/)
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1342	. . . . . . . 8 class y
9	8	csuc 4343	. . . . . . 7 class suc y
10	4, 9	wceq 1343	. . . . . 6 wff x = suc y
11	2	cv 1342	. . . . . 6 class a
12	10, 7, 11	wrex 2445	. . . . 5 wff E. y e. a x = suc y
13	6, 12	wo 698	. . . 4 wff ( x = (/) \/ E. y e. a x = suc y )
14	3, 13	wb 104	. . 3 wff ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
15	14, 1	wal 1341	. 2 wff A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
16	15, 2	wex 1480	1 wff E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )

This axiom is referenced by:  bj-omex2  13859  bj-nn0sucALT  13860