Definition df-2 9365

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 9357	. 2 class 2
2		c1 8180	. . 3 class 1
3		caddc 8182	. . 3 class +
4	2, 2, 3	co 6085	. 2 class (1 + 1)
5	1, 4	wceq 1402	1 wff 2 = (1 + 1)

This definition is used by:  2re  9376  0le2  9396  2pos  9397  1p1e2  9423  2p2e4  9433  2times  9434  3p2e5  9448  4p2e6  9450  5p2e7  9453  6p2e8  9456  7p2e9  9458  2nn  9470  1lt2  9478  nneoor  9752  6p6e12  9859  7p5e12  9862  8p2e10  9865  8p4e12  9867  9p2e11  9872  9p3e12  9873  5t2e10  9885  eluz2b1  10010  nn01to3  10026  fztp  10495  fzprval  10499  fztpval  10500  fzo12sn  10645  fzosplitpr  10662  rebtwn2zlemstep  10697  rebtwn2z  10699  sqval  11047  fac2  11183  bcp1m1  11217  hashprg  11263  binom11  12269  ege2le3  12454  ef4p  12477  efgt1p2  12478  eirraplem  12560  odd2np1lem  12655  opoe  12678  bitsfzolem  12737  ncoprmgcdne1b  12883  isprm3  12912  prmind2  12914  dvdsnprmd  12919  prmgt1  12927  pockthlem  13155  pockthg  13156  prmunb  13161  4sqlem19  13208  2expltfac  13239  mulg2  13983  dveflem  15876  coskpi  15999  ppi2  16179  ppi3  16180  ppiqeq0  16182  ppiublem2  16193  mersenne  16195  perfectlem2  16198  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  bposlem2  16210  lgslem1  16217  lgsval2lem  16227  lgsdir2lem2  16246  lgsdir2lem3  16247  lgsdirprm  16251  lgseisen  16291  m1lgs  16302  ex-fl  16837