Definition df-2 9041

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

Step	Hyp	Ref	Expression
1		c2 9033	. 2 class 2
2		c1 7873	. . 3 class 1
3		caddc 7875	. . 3 class +
4	2, 2, 3	co 5918	. 2 class ( 1 + 1 )
5	1, 4	wceq 1364	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9052  0le2  9072  2pos  9073  1p1e2  9099  2p2e4  9109  2times  9110  3p2e5  9123  4p2e6  9125  5p2e7  9128  6p2e8  9131  7p2e9  9133  2nn  9143  1lt2  9151  nneoor  9419  6p6e12  9521  7p5e12  9524  8p2e10  9527  8p4e12  9529  9p2e11  9534  9p3e12  9535  5t2e10  9547  eluz2b1  9666  nn01to3  9682  fztp  10144  fzprval  10148  fztpval  10149  fzo12sn  10284  rebtwn2zlemstep  10321  rebtwn2z  10323  sqval  10668  fac2  10802  bcp1m1  10836  hashprg  10879  binom11  11629  ege2le3  11814  ef4p  11837  efgt1p2  11838  eirraplem  11920  odd2np1lem  12013  opoe  12036  ncoprmgcdne1b  12227  isprm3  12256  prmind2  12258  dvdsnprmd  12263  prmgt1  12270  pockthlem  12494  pockthg  12495  prmunb  12500  4sqlem19  12547  gsumpr12val  12983  mulg2  13201  dveflem  14872  coskpi  14983  lgslem1  15116  lgsval2lem  15126  lgsdir2lem2  15145  lgsdir2lem3  15146  lgsdirprm  15150  lgseisen  15190  m1lgs  15192  ex-fl  15217