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

Axiom ax-inf2 11214
Description: Another axiom of infinity in a constructive setting (see ax-infvn 11179). (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 1435 . . . 4 wff 𝑥𝑎
41cv 1284 . . . . . 6 class 𝑥
5 c0 3269 . . . . . 6 class
64, 5wceq 1285 . . . . 5 wff 𝑥 = ∅
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1284 . . . . . . . 8 class 𝑦
98csuc 4156 . . . . . . 7 class suc 𝑦
104, 9wceq 1285 . . . . . 6 wff 𝑥 = suc 𝑦
112cv 1284 . . . . . 6 class 𝑎
1210, 7, 11wrex 2354 . . . . 5 wff 𝑦𝑎 𝑥 = suc 𝑦
136, 12wo 662 . . . 4 wff (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦)
143, 13wb 103 . . 3 wff (𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1514, 1wal 1283 . 2 wff 𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1615, 2wex 1422 1 wff 𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
Colors of variables: wff set class
This axiom is referenced by:  bj-omex2  11215  bj-nn0sucALT  11216
  Copyright terms: Public domain W3C validator