Definition df-2 9043

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 9035	. 2 class 2
2		c1 7875	. . 3 class 1
3		caddc 7877	. . 3 class +
4	2, 2, 3	co 5919	. 2 class ( 1 + 1 )
5	1, 4	wceq 1364	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  9054  0le2  9074  2pos  9075  1p1e2  9101  2p2e4  9111  2times  9112  3p2e5  9126  4p2e6  9128  5p2e7  9131  6p2e8  9134  7p2e9  9136  2nn  9146  1lt2  9154  nneoor  9422  6p6e12  9524  7p5e12  9527  8p2e10  9530  8p4e12  9532  9p2e11  9537  9p3e12  9538  5t2e10  9550  eluz2b1  9669  nn01to3  9685  fztp  10147  fzprval  10151  fztpval  10152  fzo12sn  10287  rebtwn2zlemstep  10324  rebtwn2z  10326  sqval  10671  fac2  10805  bcp1m1  10839  hashprg  10882  binom11  11632  ege2le3  11817  ef4p  11840  efgt1p2  11841  eirraplem  11923  odd2np1lem  12016  opoe  12039  ncoprmgcdne1b  12230  isprm3  12259  prmind2  12261  dvdsnprmd  12266  prmgt1  12273  pockthlem  12497  pockthg  12498  prmunb  12503  4sqlem19  12550  gsumpr12val  12986  mulg2  13204  dveflem  14905  coskpi  15024  lgslem1  15157  lgsval2lem  15167  lgsdir2lem2  15186  lgsdir2lem3  15187  lgsdirprm  15191  lgseisen  15231  m1lgs  15242  ex-fl  15287