Axiom ax-inf2 8079

Description: A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 8080 shows it converted to abbreviations. This axiom was derived as theorem axinf2 8078 above, using our version of Infinity ax-inf 8076 and the Axiom of Regularity ax-reg 8039. We will reference ax-inf2 8079 instead of axinf2 8078 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 8076 from ax-inf2 8079 is shown by theorem axinf 8082. (Contributed by NM, 3-Nov-1996.)

Assertion

Ref	Expression
ax-inf2

Distinct variable group:   ,,,

Detailed syntax breakdown of Axiom ax-inf2

Step	Hyp	Ref	Expression
1		vy	. . . . . 6
2		vx	. . . . . 6
3	1, 2	wel 1819	. . . . 5
4		vz	. . . . . . . 8
5	4, 1	wel 1819	. . . . . . 7
6	5	wn 3	. . . . . 6
7	6, 4	wal 1393	. . . . 5
8	3, 7	wa 369	. . . 4
9	8, 1	wex 1612	. . 3
10	4, 2	wel 1819	. . . . . . 7
11		vw	. . . . . . . . . 10
12	11, 4	wel 1819	. . . . . . . . 9
13	11, 1	wel 1819	. . . . . . . . . 10
14	11, 1	weq 1733	. . . . . . . . . 10
15	13, 14	wo 368	. . . . . . . . 9
16	12, 15	wb 184	. . . . . . . 8
17	16, 11	wal 1393	. . . . . . 7
18	10, 17	wa 369	. . . . . 6
19	18, 4	wex 1612	. . . . 5
20	3, 19	wi 4	. . . 4
21	20, 1	wal 1393	. . 3
22	9, 21	wa 369	. 2
23	22, 2	wex 1612	1

This axiom is referenced by:  zfinf2  8080