Definition df-2 9372

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 9364	. 2 class 2
2		c1 8186	. . 3 class 1
3		caddc 8188	. . 3 class +
4	2, 2, 3	co 6088	. 2 class (1 + 1)
5	1, 4	wceq 1402	1 wff 2 = (1 + 1)

This definition is used by:  2re  9383  0le2  9403  2pos  9404  1p1e2  9430  2p2e4  9440  2times  9441  3p2e5  9455  4p2e6  9457  5p2e7  9460  6p2e8  9463  7p2e9  9465  2nn  9477  1lt2  9485  nneoor  9758  6p6e12  9865  7p5e12  9868  8p2e10  9871  8p4e12  9873  9p2e11  9878  9p3e12  9879  5t2e10  9891  eluz2b1  10016  nn01to3  10032  fztp  10501  fzprval  10505  fztpval  10506  fzo12sn  10651  fzosplitpr  10668  rebtwn2zlemstep  10703  rebtwn2z  10705  sqval  11054  fac2  11190  bcp1m1  11224  hashprg  11270  binom11  12277  ege2le3  12462  ef4p  12485  efgt1p2  12486  eirraplem  12568  odd2np1lem  12663  opoe  12686  bitsfzolem  12745  ncoprmgcdne1b  12891  isprm3  12920  prmind2  12922  dvdsnprmd  12927  prmgt1  12935  pockthlem  13163  pockthg  13164  prmunb  13169  4sqlem19  13216  2expltfac  13247  mulg2  13992  dveflem  15969  coskpi  16092  ppi2  16291  ppi3  16292  cht2  16293  ppiqeq0  16297  ppiublem2  16309  chtqub  16313  mersenne  16314  perfectlem2  16317  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem6  16333  lgslem1  16341  lgsval2lem  16351  lgsdir2lem2  16370  lgsdir2lem3  16371  lgsdirprm  16375  lgseisen  16415  m1lgs  16426  ex-fl  16961