Definition df-2 9180

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 9172	. 2 class 2
2		c1 8011	. . 3 class 1
3		caddc 8013	. . 3 class +
4	2, 2, 3	co 6007	. 2 class (1 + 1)
5	1, 4	wceq 1395	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9191  0le2  9211  2pos  9212  1p1e2  9238  2p2e4  9248  2times  9249  3p2e5  9263  4p2e6  9265  5p2e7  9268  6p2e8  9271  7p2e9  9273  2nn  9283  1lt2  9291  nneoor  9560  6p6e12  9662  7p5e12  9665  8p2e10  9668  8p4e12  9670  9p2e11  9675  9p3e12  9676  5t2e10  9688  eluz2b1  9808  nn01to3  9824  fztp  10286  fzprval  10290  fztpval  10291  fzo12sn  10435  rebtwn2zlemstep  10484  rebtwn2z  10486  sqval  10831  fac2  10965  bcp1m1  10999  hashprg  11043  binom11  12012  ege2le3  12197  ef4p  12220  efgt1p2  12221  eirraplem  12303  odd2np1lem  12398  opoe  12421  bitsfzolem  12480  ncoprmgcdne1b  12626  isprm3  12655  prmind2  12657  dvdsnprmd  12662  prmgt1  12669  pockthlem  12894  pockthg  12895  prmunb  12900  4sqlem19  12947  2expltfac  12977  gsumpr12val  13448  mulg2  13683  dveflem  15415  coskpi  15537  mersenne  15686  perfectlem2  15689  lgslem1  15694  lgsval2lem  15704  lgsdir2lem2  15723  lgsdir2lem3  15724  lgsdirprm  15728  lgseisen  15768  m1lgs  15779  ex-fl  16144