Definition df-2 9372

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 9364	. 2 class 2
2		c1 8186	. . 3 class 1
3		caddc 8188	. . 3 class +
4	2, 2, 3	co 6088	. 2 class (1 + 1)
5	1, 4	wceq 1402	1 wff 2 = (1 + 1)

This definition is used by:  2re  9383  0le2  9403  2pos  9404  1p1e2  9430  2p2e4  9440  2times  9441  3p2e5  9455  4p2e6  9457  5p2e7  9460  6p2e8  9463  7p2e9  9465  2nn  9477  1lt2  9485  nneoor  9759  6p6e12  9866  7p5e12  9869  8p2e10  9872  8p4e12  9874  9p2e11  9879  9p3e12  9880  5t2e10  9892  eluz2b1  10017  nn01to3  10033  fztp  10502  fzprval  10506  fztpval  10507  fzo12sn  10652  fzosplitpr  10669  rebtwn2zlemstep  10704  rebtwn2z  10706  sqval  11055  fac2  11191  bcp1m1  11225  hashprg  11271  binom11  12278  ege2le3  12463  ef4p  12486  efgt1p2  12487  eirraplem  12569  odd2np1lem  12664  opoe  12687  bitsfzolem  12746  ncoprmgcdne1b  12892  isprm3  12921  prmind2  12923  dvdsnprmd  12928  prmgt1  12936  pockthlem  13164  pockthg  13165  prmunb  13170  4sqlem19  13217  2expltfac  13248  mulg2  13993  dveflem  15952  coskpi  16075  ppi2  16274  ppi3  16275  cht2  16276  ppiqeq0  16280  ppiublem2  16292  chtqub  16296  mersenne  16297  perfectlem2  16300  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  bposlem2  16312  bposlem6  16316  lgslem1  16324  lgsval2lem  16334  lgsdir2lem2  16353  lgsdir2lem3  16354  lgsdirprm  16358  lgseisen  16398  m1lgs  16409  ex-fl  16944