Definition df-2 9097

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

This definition is referenced by:  2re  9108  0le2  9128  2pos  9129  1p1e2  9155  2p2e4  9165  2times  9166  3p2e5  9180  4p2e6  9182  5p2e7  9185  6p2e8  9188  7p2e9  9190  2nn  9200  1lt2  9208  nneoor  9477  6p6e12  9579  7p5e12  9582  8p2e10  9585  8p4e12  9587  9p2e11  9592  9p3e12  9593  5t2e10  9605  eluz2b1  9724  nn01to3  9740  fztp  10202  fzprval  10206  fztpval  10207  fzo12sn  10348  rebtwn2zlemstep  10397  rebtwn2z  10399  sqval  10744  fac2  10878  bcp1m1  10912  hashprg  10955  binom11  11830  ege2le3  12015  ef4p  12038  efgt1p2  12039  eirraplem  12121  odd2np1lem  12216  opoe  12239  bitsfzolem  12298  ncoprmgcdne1b  12444  isprm3  12473  prmind2  12475  dvdsnprmd  12480  prmgt1  12487  pockthlem  12712  pockthg  12713  prmunb  12718  4sqlem19  12765  2expltfac  12795  gsumpr12val  13265  mulg2  13500  dveflem  15231  coskpi  15353  mersenne  15502  perfectlem2  15505  lgslem1  15510  lgsval2lem  15520  lgsdir2lem2  15539  lgsdir2lem3  15540  lgsdirprm  15544  lgseisen  15584  m1lgs  15595  ex-fl  15698