Definition df-2 8542

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 8534	. 2 class 2
2		c1 7412	. . 3 class 1
3		caddc 7414	. . 3 class +
4	2, 2, 3	co 5666	. 2 class (1 + 1)
5	1, 4	wceq 1290	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  8553  0le2  8573  2pos  8574  1p1e2  8600  2p2e4  8604  2times  8605  3p2e5  8618  4p2e6  8620  5p2e7  8623  6p2e8  8626  7p2e9  8628  2nn  8638  1lt2  8646  nneoor  8909  6p6e12  9011  7p5e12  9014  8p2e10  9017  8p4e12  9019  9p2e11  9024  9p3e12  9025  5t2e10  9037  eluz2b1  9149  nn01to3  9163  fztp  9553  fzprval  9557  fztpval  9558  fzo12sn  9689  rebtwn2zlemstep  9725  rebtwn2z  9727  sqval  10074  fac2  10200  bcp1m1  10234  hashprg  10277  binom11  10941  ege2le3  11022  ef4p  11045  efgt1p2  11046  eirraplem  11125  odd2np1lem  11211  opoe  11234  ncoprmgcdne1b  11410  isprm3  11439  prmind2  11441  dvdsnprmd  11446  prmgt1  11452  ex-fl  11925