Definition df-2 9165

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 9157	. 2 class 2
2		c1 7996	. . 3 class 1
3		caddc 7998	. . 3 class +
4	2, 2, 3	co 6000	. 2 class (1 + 1)
5	1, 4	wceq 1395	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9176  0le2  9196  2pos  9197  1p1e2  9223  2p2e4  9233  2times  9234  3p2e5  9248  4p2e6  9250  5p2e7  9253  6p2e8  9256  7p2e9  9258  2nn  9268  1lt2  9276  nneoor  9545  6p6e12  9647  7p5e12  9650  8p2e10  9653  8p4e12  9655  9p2e11  9660  9p3e12  9661  5t2e10  9673  eluz2b1  9792  nn01to3  9808  fztp  10270  fzprval  10274  fztpval  10275  fzo12sn  10418  rebtwn2zlemstep  10467  rebtwn2z  10469  sqval  10814  fac2  10948  bcp1m1  10982  hashprg  11025  binom11  11992  ege2le3  12177  ef4p  12200  efgt1p2  12201  eirraplem  12283  odd2np1lem  12378  opoe  12401  bitsfzolem  12460  ncoprmgcdne1b  12606  isprm3  12635  prmind2  12637  dvdsnprmd  12642  prmgt1  12649  pockthlem  12874  pockthg  12875  prmunb  12880  4sqlem19  12927  2expltfac  12957  gsumpr12val  13428  mulg2  13663  dveflem  15394  coskpi  15516  mersenne  15665  perfectlem2  15668  lgslem1  15673  lgsval2lem  15683  lgsdir2lem2  15702  lgsdir2lem3  15703  lgsdirprm  15707  lgseisen  15747  m1lgs  15758  ex-fl  16047