Definition df-2 9068

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 9060	. 2 class 2
2		c1 7899	. . 3 class 1
3		caddc 7901	. . 3 class +
4	2, 2, 3	co 5925	. 2 class (1 + 1)
5	1, 4	wceq 1364	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9079  0le2  9099  2pos  9100  1p1e2  9126  2p2e4  9136  2times  9137  3p2e5  9151  4p2e6  9153  5p2e7  9156  6p2e8  9159  7p2e9  9161  2nn  9171  1lt2  9179  nneoor  9447  6p6e12  9549  7p5e12  9552  8p2e10  9555  8p4e12  9557  9p2e11  9562  9p3e12  9563  5t2e10  9575  eluz2b1  9694  nn01to3  9710  fztp  10172  fzprval  10176  fztpval  10177  fzo12sn  10312  rebtwn2zlemstep  10361  rebtwn2z  10363  sqval  10708  fac2  10842  bcp1m1  10876  hashprg  10919  binom11  11670  ege2le3  11855  ef4p  11878  efgt1p2  11879  eirraplem  11961  odd2np1lem  12056  opoe  12079  bitsfzolem  12138  ncoprmgcdne1b  12284  isprm3  12313  prmind2  12315  dvdsnprmd  12320  prmgt1  12327  pockthlem  12552  pockthg  12553  prmunb  12558  4sqlem19  12605  2expltfac  12635  gsumpr12val  13104  mulg2  13339  dveflem  15070  coskpi  15192  mersenne  15341  perfectlem2  15344  lgslem1  15349  lgsval2lem  15359  lgsdir2lem2  15378  lgsdir2lem3  15379  lgsdirprm  15383  lgseisen  15423  m1lgs  15434  ex-fl  15479