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

Axiom ax-inf2 11871
Description: Another axiom of infinity in a constructive setting (see ax-infvn 11836). (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 1439 . . . 4  wff  x  e.  a
41cv 1288 . . . . . 6  class  x
5 c0 3286 . . . . . 6  class  (/)
64, 5wceq 1289 . . . . 5  wff  x  =  (/)
7 vy . . . . . . . . 9  setvar  y
87cv 1288 . . . . . . . 8  class  y
98csuc 4192 . . . . . . 7  class  suc  y
104, 9wceq 1289 . . . . . 6  wff  x  =  suc  y
112cv 1288 . . . . . 6  class  a
1210, 7, 11wrex 2360 . . . . 5  wff  E. y  e.  a  x  =  suc  y
136, 12wo 664 . . . 4  wff  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y )
143, 13wb 103 . . 3  wff  ( x  e.  a  <->  ( x  =  (/)  \/  E. y  e.  a  x  =  suc  y ) )
1514, 1wal 1287 . 2  wff  A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
1615, 2wex 1426 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  11872  bj-nn0sucALT  11873
  Copyright terms: Public domain W3C validator