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

Axiom ax-inf2 13101
Description: Another axiom of infinity in a constructive setting (see ax-infvn 13066). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.)
Assertion
Ref Expression
ax-inf2  |-  E. a A. x ( x  e.  a  <->  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Axiom ax-inf2
StepHypRef Expression
1 vx . . . . 5  setvar  x
2 va . . . . 5  setvar  a
31, 2wel 1466 . . . 4  wff  x  e.  a
41cv 1315 . . . . . 6  class  x
5 c0 3333 . . . . . 6  class  (/)
64, 5wceq 1316 . . . . 5  wff  x  =  (/)
7 vy . . . . . . . . 9  setvar  y
87cv 1315 . . . . . . . 8  class  y
98csuc 4257 . . . . . . 7  class  suc  y
104, 9wceq 1316 . . . . . 6  wff  x  =  suc  y
112cv 1315 . . . . . 6  class  a
1210, 7, 11wrex 2394 . . . . 5  wff  E. y  e.  a  x  =  suc  y
136, 12wo 682 . . . 4  wff  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y )
143, 13wb 104 . . 3  wff  ( x  e.  a  <->  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y ) )
1514, 1wal 1314 . 2  wff  A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
1615, 2wex 1453 1  wff  E. a A. x ( x  e.  a  <->  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y ) )
Colors of variables: wff set class
This axiom is referenced by:  bj-omex2  13102  bj-nn0sucALT  13103
  Copyright terms: Public domain W3C validator