Definition df-2 8803

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 8795	. 2 class 2
2		c1 7645	. . 3 class 1
3		caddc 7647	. . 3 class +
4	2, 2, 3	co 5782	. 2 class ( 1 + 1 )
5	1, 4	wceq 1332	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8814  0le2  8834  2pos  8835  1p1e2  8861  2p2e4  8871  2times  8872  3p2e5  8885  4p2e6  8887  5p2e7  8890  6p2e8  8893  7p2e9  8895  2nn  8905  1lt2  8913  nneoor  9177  6p6e12  9279  7p5e12  9282  8p2e10  9285  8p4e12  9287  9p2e11  9292  9p3e12  9293  5t2e10  9305  eluz2b1  9422  nn01to3  9436  fztp  9889  fzprval  9893  fztpval  9894  fzo12sn  10025  rebtwn2zlemstep  10061  rebtwn2z  10063  sqval  10382  fac2  10509  bcp1m1  10543  hashprg  10586  binom11  11287  ege2le3  11414  ef4p  11437  efgt1p2  11438  eirraplem  11519  odd2np1lem  11605  opoe  11628  ncoprmgcdne1b  11806  isprm3  11835  prmind2  11837  dvdsnprmd  11842  prmgt1  11848  dveflem  12895  coskpi  12977  ex-fl  13108