ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-2 Unicode version

Definition df-2 8791
Description: Define the number 2. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-2  |-  2  =  ( 1  +  1 )

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 8783 . 2  class  2
2 c1 7633 . . 3  class  1
3 caddc 7635 . . 3  class  +
42, 2, 3co 5774 . 2  class  ( 1  +  1 )
51, 4wceq 1331 1  wff  2  =  ( 1  +  1 )
Colors of variables: wff set class
This definition is referenced by:  2re  8802  0le2  8822  2pos  8823  1p1e2  8849  2p2e4  8859  2times  8860  3p2e5  8873  4p2e6  8875  5p2e7  8878  6p2e8  8881  7p2e9  8883  2nn  8893  1lt2  8901  nneoor  9165  6p6e12  9267  7p5e12  9270  8p2e10  9273  8p4e12  9275  9p2e11  9280  9p3e12  9281  5t2e10  9293  eluz2b1  9407  nn01to3  9421  fztp  9870  fzprval  9874  fztpval  9875  fzo12sn  10006  rebtwn2zlemstep  10042  rebtwn2z  10044  sqval  10363  fac2  10489  bcp1m1  10523  hashprg  10566  binom11  11267  ege2le3  11389  ef4p  11412  efgt1p2  11413  eirraplem  11494  odd2np1lem  11580  opoe  11603  ncoprmgcdne1b  11781  isprm3  11810  prmind2  11812  dvdsnprmd  11817  prmgt1  11823  dveflem  12870  coskpi  12951  ex-fl  13042
  Copyright terms: Public domain W3C validator