Definition df-2 9201

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 9193	. 2 class 2
2		c1 8032	. . 3 class 1
3		caddc 8034	. . 3 class +
4	2, 2, 3	co 6017	. 2 class (1 + 1)
5	1, 4	wceq 1397	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9212  0le2  9232  2pos  9233  1p1e2  9259  2p2e4  9269  2times  9270  3p2e5  9284  4p2e6  9286  5p2e7  9289  6p2e8  9292  7p2e9  9294  2nn  9304  1lt2  9312  nneoor  9581  6p6e12  9683  7p5e12  9686  8p2e10  9689  8p4e12  9691  9p2e11  9696  9p3e12  9697  5t2e10  9709  eluz2b1  9834  nn01to3  9850  fztp  10312  fzprval  10316  fztpval  10317  fzo12sn  10461  fzosplitpr  10478  rebtwn2zlemstep  10511  rebtwn2z  10513  sqval  10858  fac2  10992  bcp1m1  11026  hashprg  11071  binom11  12046  ege2le3  12231  ef4p  12254  efgt1p2  12255  eirraplem  12337  odd2np1lem  12432  opoe  12455  bitsfzolem  12514  ncoprmgcdne1b  12660  isprm3  12689  prmind2  12691  dvdsnprmd  12696  prmgt1  12703  pockthlem  12928  pockthg  12929  prmunb  12934  4sqlem19  12981  2expltfac  13011  gsumpr12val  13482  mulg2  13717  dveflem  15449  coskpi  15571  mersenne  15720  perfectlem2  15723  lgslem1  15728  lgsval2lem  15738  lgsdir2lem2  15757  lgsdir2lem3  15758  lgsdirprm  15762  lgseisen  15802  m1lgs  15813  ex-fl  16321