Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-inf2 GIF version

Axiom ax-inf2 11517
Description: Another axiom of infinity in a constructive setting (see ax-infvn 11482). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
Assertion
Ref Expression
ax-inf2 𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-inf2
StepHypRef Expression
1 vx . . . . 5 setvar 𝑥
2 va . . . . 5 setvar 𝑎
31, 2wel 1439 . . . 4 wff 𝑥𝑎
41cv 1288 . . . . . 6 class 𝑥
5 c0 3284 . . . . . 6 class
64, 5wceq 1289 . . . . 5 wff 𝑥 = ∅
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1288 . . . . . . . 8 class 𝑦
98csuc 4183 . . . . . . 7 class suc 𝑦
104, 9wceq 1289 . . . . . 6 wff 𝑥 = suc 𝑦
112cv 1288 . . . . . 6 class 𝑎
1210, 7, 11wrex 2360 . . . . 5 wff 𝑦𝑎 𝑥 = suc 𝑦
136, 12wo 664 . . . 4 wff (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦)
143, 13wb 103 . . 3 wff (𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1514, 1wal 1287 . 2 wff 𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1615, 2wex 1426 1 wff 𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
Colors of variables: wff set class
This axiom is referenced by:  bj-omex2  11518  bj-nn0sucALT  11519
  Copyright terms: Public domain W3C validator