Definition df-2 9130

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 9122	. 2 class 2
2		c1 7961	. . 3 class 1
3		caddc 7963	. . 3 class +
4	2, 2, 3	co 5967	. 2 class ( 1 + 1 )
5	1, 4	wceq 1373	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9141  0le2  9161  2pos  9162  1p1e2  9188  2p2e4  9198  2times  9199  3p2e5  9213  4p2e6  9215  5p2e7  9218  6p2e8  9221  7p2e9  9223  2nn  9233  1lt2  9241  nneoor  9510  6p6e12  9612  7p5e12  9615  8p2e10  9618  8p4e12  9620  9p2e11  9625  9p3e12  9626  5t2e10  9638  eluz2b1  9757  nn01to3  9773  fztp  10235  fzprval  10239  fztpval  10240  fzo12sn  10383  rebtwn2zlemstep  10432  rebtwn2z  10434  sqval  10779  fac2  10913  bcp1m1  10947  hashprg  10990  binom11  11912  ege2le3  12097  ef4p  12120  efgt1p2  12121  eirraplem  12203  odd2np1lem  12298  opoe  12321  bitsfzolem  12380  ncoprmgcdne1b  12526  isprm3  12555  prmind2  12557  dvdsnprmd  12562  prmgt1  12569  pockthlem  12794  pockthg  12795  prmunb  12800  4sqlem19  12847  2expltfac  12877  gsumpr12val  13347  mulg2  13582  dveflem  15313  coskpi  15435  mersenne  15584  perfectlem2  15587  lgslem1  15592  lgsval2lem  15602  lgsdir2lem2  15621  lgsdir2lem3  15622  lgsdirprm  15626  lgseisen  15666  m1lgs  15677  ex-fl  15861