Definition df-2 8779

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 8771	. 2 class 2
2		c1 7621	. . 3 class 1
3		caddc 7623	. . 3 class +
4	2, 2, 3	co 5774	. 2 class ( 1 + 1 )
5	1, 4	wceq 1331	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8790  0le2  8810  2pos  8811  1p1e2  8837  2p2e4  8847  2times  8848  3p2e5  8861  4p2e6  8863  5p2e7  8866  6p2e8  8869  7p2e9  8871  2nn  8881  1lt2  8889  nneoor  9153  6p6e12  9255  7p5e12  9258  8p2e10  9261  8p4e12  9263  9p2e11  9268  9p3e12  9269  5t2e10  9281  eluz2b1  9395  nn01to3  9409  fztp  9858  fzprval  9862  fztpval  9863  fzo12sn  9994  rebtwn2zlemstep  10030  rebtwn2z  10032  sqval  10351  fac2  10477  bcp1m1  10511  hashprg  10554  binom11  11255  ege2le3  11377  ef4p  11400  efgt1p2  11401  eirraplem  11483  odd2np1lem  11569  opoe  11592  ncoprmgcdne1b  11770  isprm3  11799  prmind2  11801  dvdsnprmd  11806  prmgt1  11812  dveflem  12855  coskpi  12929  ex-fl  12937