Definition df-2 9009

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 9001	. 2 class 2
2		c1 7843	. . 3 class 1
3		caddc 7845	. . 3 class +
4	2, 2, 3	co 5897	. 2 class ( 1 + 1 )
5	1, 4	wceq 1364	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9020  0le2  9040  2pos  9041  1p1e2  9067  2p2e4  9077  2times  9078  3p2e5  9091  4p2e6  9093  5p2e7  9096  6p2e8  9099  7p2e9  9101  2nn  9111  1lt2  9119  nneoor  9386  6p6e12  9488  7p5e12  9491  8p2e10  9494  8p4e12  9496  9p2e11  9501  9p3e12  9502  5t2e10  9514  eluz2b1  9633  nn01to3  9649  fztp  10110  fzprval  10114  fztpval  10115  fzo12sn  10249  rebtwn2zlemstep  10285  rebtwn2z  10287  sqval  10612  fac2  10746  bcp1m1  10780  hashprg  10823  binom11  11529  ege2le3  11714  ef4p  11737  efgt1p2  11738  eirraplem  11819  odd2np1lem  11912  opoe  11935  ncoprmgcdne1b  12124  isprm3  12153  prmind2  12155  dvdsnprmd  12160  prmgt1  12167  pockthlem  12391  pockthg  12392  prmunb  12397  4sqlem19  12444  gsumpr12val  12878  mulg2  13088  dveflem  14664  coskpi  14746  lgslem1  14879  lgsval2lem  14889  lgsdir2lem2  14908  lgsdir2lem3  14909  lgsdirprm  14913  m1lgs  14930  ex-fl  14955