Axiom ax-inf2 14011

Description: Another axiom of infinity in a constructive setting (see ax-infvn 13976). (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 2142	. . . 4 wff x e. a
4	1	cv 1347	. . . . . 6 class x
5		c0 3414	. . . . . 6 class (/)
6	4, 5	wceq 1348	. . . . 5 wff x = (/)
7		vy	. . . . . . . . 9 setvar y
8	7	cv 1347	. . . . . . . 8 class y
9	8	csuc 4350	. . . . . . 7 class suc y
10	4, 9	wceq 1348	. . . . . 6 wff x = suc y
11	2	cv 1347	. . . . . 6 class a
12	10, 7, 11	wrex 2449	. . . . 5 wff E. y e. a x = suc y
13	6, 12	wo 703	. . . 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 1346	. 2 wff A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )
16	15, 2	wex 1485	1 wff E. a A. x ( x e. a <-> ( x = (/) \/ E. y e. a x = suc y ) )

This axiom is referenced by:  bj-omex2  14012  bj-nn0sucALT  14013