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

Axiom ax-inf2 10101
Description: Another axiom of infinity in a constructive setting (see ax-infvn 10066). (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 1394 . . . 4 wff 𝑥𝑎
41cv 1242 . . . . . 6 class 𝑥
5 c0 3224 . . . . . 6 class
64, 5wceq 1243 . . . . 5 wff 𝑥 = ∅
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1242 . . . . . . . 8 class 𝑦
98csuc 4102 . . . . . . 7 class suc 𝑦
104, 9wceq 1243 . . . . . 6 wff 𝑥 = suc 𝑦
112cv 1242 . . . . . 6 class 𝑎
1210, 7, 11wrex 2307 . . . . 5 wff 𝑦𝑎 𝑥 = suc 𝑦
136, 12wo 629 . . . 4 wff (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦)
143, 13wb 98 . . 3 wff (𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1514, 1wal 1241 . 2 wff 𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
1615, 2wex 1381 1 wff 𝑎𝑥(𝑥𝑎 ↔ (𝑥 = ∅ ∨ ∃𝑦𝑎 𝑥 = suc 𝑦))
Colors of variables: wff set class
This axiom is referenced by:  bj-omex2  10102  bj-nn0sucALT  10103
  Copyright terms: Public domain W3C validator