Definition df-2 8977

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 8969	. 2 class 2
2		c1 7811	. . 3 class 1
3		caddc 7813	. . 3 class +
4	2, 2, 3	co 5874	. 2 class (1 + 1)
5	1, 4	wceq 1353	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  8988  0le2  9008  2pos  9009  1p1e2  9035  2p2e4  9045  2times  9046  3p2e5  9059  4p2e6  9061  5p2e7  9064  6p2e8  9067  7p2e9  9069  2nn  9079  1lt2  9087  nneoor  9354  6p6e12  9456  7p5e12  9459  8p2e10  9462  8p4e12  9464  9p2e11  9469  9p3e12  9470  5t2e10  9482  eluz2b1  9600  nn01to3  9616  fztp  10077  fzprval  10081  fztpval  10082  fzo12sn  10216  rebtwn2zlemstep  10252  rebtwn2z  10254  sqval  10577  fac2  10710  bcp1m1  10744  hashprg  10787  binom11  11493  ege2le3  11678  ef4p  11701  efgt1p2  11702  eirraplem  11783  odd2np1lem  11876  opoe  11899  ncoprmgcdne1b  12088  isprm3  12117  prmind2  12119  dvdsnprmd  12124  prmgt1  12131  pockthlem  12353  pockthg  12354  prmunb  12359  mulg2  12991  dveflem  14157  coskpi  14239  lgslem1  14371  lgsval2lem  14381  lgsdir2lem2  14400  lgsdir2lem3  14401  lgsdirprm  14405  m1lgs  14422  ex-fl  14447