Definition df-2 8772

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 8764	. 2 class 2
2		c1 7614	. . 3 class 1
3		caddc 7616	. . 3 class +
4	2, 2, 3	co 5767	. 2 class (1 + 1)
5	1, 4	wceq 1331	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  8783  0le2  8803  2pos  8804  1p1e2  8830  2p2e4  8840  2times  8841  3p2e5  8854  4p2e6  8856  5p2e7  8859  6p2e8  8862  7p2e9  8864  2nn  8874  1lt2  8882  nneoor  9146  6p6e12  9248  7p5e12  9251  8p2e10  9254  8p4e12  9256  9p2e11  9261  9p3e12  9262  5t2e10  9274  eluz2b1  9388  nn01to3  9402  fztp  9851  fzprval  9855  fztpval  9856  fzo12sn  9987  rebtwn2zlemstep  10023  rebtwn2z  10025  sqval  10344  fac2  10470  bcp1m1  10504  hashprg  10547  binom11  11248  ege2le3  11366  ef4p  11389  efgt1p2  11390  eirraplem  11472  odd2np1lem  11558  opoe  11581  ncoprmgcdne1b  11759  isprm3  11788  prmind2  11790  dvdsnprmd  11795  prmgt1  11801  dveflem  12844  coskpi  12918  ex-fl  12926