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

Definition df-2 7971
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 7962 . 2 class 2
2 c1 6888 . . 3 class 1
3 caddc 6890 . . 3 class +
42, 2, 3co 5512 . 2 class (1 + 1)
51, 4wceq 1243 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re  7983  0le2  8004  2pos  8005  1p1e2  8031  2p2e4  8035  2times  8036  3p2e5  8050  4p2e6  8052  5p2e7  8055  6p2e8  8059  7p2e9  8062  8p2e10  8064  2nn  8075  1lt2  8084  nneoor  8338  6p6e12  8416  7p5e12  8418  8p4e12  8422  9p2e11  8427  9p3e12  8428  eluz2b1  8537  nn01to3  8550  fztp  8938  fzprval  8942  fztpval  8943  fzo12sn  9071  rebtwn2zlemstep  9105  rebtwn2z  9107  sqval  9286  ex-fl  9869
  Copyright terms: Public domain W3C validator