MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-inf2 Unicode version

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
StepHypRef Expression
1 vy . . . . . 6
2 vx . . . . . 6
31, 2wel 1819 . . . . 5
4 vz . . . . . . . 8
54, 1wel 1819 . . . . . . 7
65wn 3 . . . . . 6
76, 4wal 1393 . . . . 5
83, 7wa 369 . . . 4
98, 1wex 1612 . . 3
104, 2wel 1819 . . . . . . 7
11 vw . . . . . . . . . 10
1211, 4wel 1819 . . . . . . . . 9
1311, 1wel 1819 . . . . . . . . . 10
1411, 1weq 1733 . . . . . . . . . 10
1513, 14wo 368 . . . . . . . . 9
1612, 15wb 184 . . . . . . . 8
1716, 11wal 1393 . . . . . . 7
1810, 17wa 369 . . . . . 6
1918, 4wex 1612 . . . . 5
203, 19wi 4 . . . 4
2120, 1wal 1393 . . 3
229, 21wa 369 . 2
2322, 2wex 1612 1
Colors of variables: wff setvar class
This axiom is referenced by:  zfinf2  8080
  Copyright terms: Public domain W3C validator