Definition df-2 9115

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 9107	. 2 class 2
2		c1 7946	. . 3 class 1
3		caddc 7948	. . 3 class +
4	2, 2, 3	co 5957	. 2 class (1 + 1)
5	1, 4	wceq 1373	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9126  0le2  9146  2pos  9147  1p1e2  9173  2p2e4  9183  2times  9184  3p2e5  9198  4p2e6  9200  5p2e7  9203  6p2e8  9206  7p2e9  9208  2nn  9218  1lt2  9226  nneoor  9495  6p6e12  9597  7p5e12  9600  8p2e10  9603  8p4e12  9605  9p2e11  9610  9p3e12  9611  5t2e10  9623  eluz2b1  9742  nn01to3  9758  fztp  10220  fzprval  10224  fztpval  10225  fzo12sn  10368  rebtwn2zlemstep  10417  rebtwn2z  10419  sqval  10764  fac2  10898  bcp1m1  10932  hashprg  10975  binom11  11872  ege2le3  12057  ef4p  12080  efgt1p2  12081  eirraplem  12163  odd2np1lem  12258  opoe  12281  bitsfzolem  12340  ncoprmgcdne1b  12486  isprm3  12515  prmind2  12517  dvdsnprmd  12522  prmgt1  12529  pockthlem  12754  pockthg  12755  prmunb  12760  4sqlem19  12807  2expltfac  12837  gsumpr12val  13307  mulg2  13542  dveflem  15273  coskpi  15395  mersenne  15544  perfectlem2  15547  lgslem1  15552  lgsval2lem  15562  lgsdir2lem2  15581  lgsdir2lem3  15582  lgsdirprm  15586  lgseisen  15626  m1lgs  15637  ex-fl  15800