Definition df-2 9095

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 9087	. 2 class 2
2		c1 7926	. . 3 class 1
3		caddc 7928	. . 3 class +
4	2, 2, 3	co 5944	. 2 class ( 1 + 1 )
5	1, 4	wceq 1373	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9106  0le2  9126  2pos  9127  1p1e2  9153  2p2e4  9163  2times  9164  3p2e5  9178  4p2e6  9180  5p2e7  9183  6p2e8  9186  7p2e9  9188  2nn  9198  1lt2  9206  nneoor  9475  6p6e12  9577  7p5e12  9580  8p2e10  9583  8p4e12  9585  9p2e11  9590  9p3e12  9591  5t2e10  9603  eluz2b1  9722  nn01to3  9738  fztp  10200  fzprval  10204  fztpval  10205  fzo12sn  10346  rebtwn2zlemstep  10395  rebtwn2z  10397  sqval  10742  fac2  10876  bcp1m1  10910  hashprg  10953  binom11  11797  ege2le3  11982  ef4p  12005  efgt1p2  12006  eirraplem  12088  odd2np1lem  12183  opoe  12206  bitsfzolem  12265  ncoprmgcdne1b  12411  isprm3  12440  prmind2  12442  dvdsnprmd  12447  prmgt1  12454  pockthlem  12679  pockthg  12680  prmunb  12685  4sqlem19  12732  2expltfac  12762  gsumpr12val  13232  mulg2  13467  dveflem  15198  coskpi  15320  mersenne  15469  perfectlem2  15472  lgslem1  15477  lgsval2lem  15487  lgsdir2lem2  15506  lgsdir2lem3  15507  lgsdirprm  15511  lgseisen  15551  m1lgs  15562  ex-fl  15661