Definition df-2 8951

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 8943	. 2 class 2
2		c1 7787	. . 3 class 1
3		caddc 7789	. . 3 class +
4	2, 2, 3	co 5865	. 2 class ( 1 + 1 )
5	1, 4	wceq 1353	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8962  0le2  8982  2pos  8983  1p1e2  9009  2p2e4  9019  2times  9020  3p2e5  9033  4p2e6  9035  5p2e7  9038  6p2e8  9041  7p2e9  9043  2nn  9053  1lt2  9061  nneoor  9328  6p6e12  9430  7p5e12  9433  8p2e10  9436  8p4e12  9438  9p2e11  9443  9p3e12  9444  5t2e10  9456  eluz2b1  9574  nn01to3  9590  fztp  10048  fzprval  10052  fztpval  10053  fzo12sn  10187  rebtwn2zlemstep  10223  rebtwn2z  10225  sqval  10548  fac2  10679  bcp1m1  10713  hashprg  10756  binom11  11462  ege2le3  11647  ef4p  11670  efgt1p2  11671  eirraplem  11752  odd2np1lem  11844  opoe  11867  ncoprmgcdne1b  12056  isprm3  12085  prmind2  12087  dvdsnprmd  12092  prmgt1  12099  pockthlem  12321  pockthg  12322  prmunb  12327  mulg2  12862  dveflem  13767  coskpi  13849  lgslem1  13981  lgsval2lem  13991  lgsdir2lem2  14010  lgsdir2lem3  14011  lgsdirprm  14015  ex-fl  14046