Definition df-2 8978

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 8970	. 2 class 2
2		c1 7812	. . 3 class 1
3		caddc 7814	. . 3 class +
4	2, 2, 3	co 5875	. 2 class (1 + 1)
5	1, 4	wceq 1353	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  8989  0le2  9009  2pos  9010  1p1e2  9036  2p2e4  9046  2times  9047  3p2e5  9060  4p2e6  9062  5p2e7  9065  6p2e8  9068  7p2e9  9070  2nn  9080  1lt2  9088  nneoor  9355  6p6e12  9457  7p5e12  9460  8p2e10  9463  8p4e12  9465  9p2e11  9470  9p3e12  9471  5t2e10  9483  eluz2b1  9601  nn01to3  9617  fztp  10078  fzprval  10082  fztpval  10083  fzo12sn  10217  rebtwn2zlemstep  10253  rebtwn2z  10255  sqval  10578  fac2  10711  bcp1m1  10745  hashprg  10788  binom11  11494  ege2le3  11679  ef4p  11702  efgt1p2  11703  eirraplem  11784  odd2np1lem  11877  opoe  11900  ncoprmgcdne1b  12089  isprm3  12118  prmind2  12120  dvdsnprmd  12125  prmgt1  12132  pockthlem  12354  pockthg  12355  prmunb  12360  mulg2  12992  dveflem  14190  coskpi  14272  lgslem1  14404  lgsval2lem  14414  lgsdir2lem2  14433  lgsdir2lem3  14434  lgsdirprm  14438  m1lgs  14455  ex-fl  14480