Definition df-2 9298

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 9290	. 2 class 2
2		c1 8130	. . 3 class 1
3		caddc 8132	. . 3 class +
4	2, 2, 3	co 6052	. 2 class ( 1 + 1 )
5	1, 4	wceq 1398	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9309  0le2  9329  2pos  9330  1p1e2  9356  2p2e4  9366  2times  9367  3p2e5  9381  4p2e6  9383  5p2e7  9386  6p2e8  9389  7p2e9  9391  2nn  9401  1lt2  9409  nneoor  9683  6p6e12  9785  7p5e12  9788  8p2e10  9791  8p4e12  9793  9p2e11  9798  9p3e12  9799  5t2e10  9811  eluz2b1  9936  nn01to3  9952  fztp  10416  fzprval  10420  fztpval  10421  fzo12sn  10566  fzosplitpr  10583  rebtwn2zlemstep  10616  rebtwn2z  10618  sqval  10963  fac2  11097  bcp1m1  11131  hashprg  11177  binom11  12176  ege2le3  12361  ef4p  12384  efgt1p2  12385  eirraplem  12467  odd2np1lem  12562  opoe  12585  bitsfzolem  12644  ncoprmgcdne1b  12790  isprm3  12819  prmind2  12821  dvdsnprmd  12826  prmgt1  12833  pockthlem  13058  pockthg  13059  prmunb  13064  4sqlem19  13111  2expltfac  13141  gsumpr12val  13630  mulg2  13865  dveflem  15608  coskpi  15730  mersenne  15882  perfectlem2  15885  lgslem1  15890  lgsval2lem  15900  lgsdir2lem2  15919  lgsdir2lem3  15920  lgsdirprm  15924  lgseisen  15964  m1lgs  15975  ex-fl  16510