Definition df-2 8980

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 8972	. 2 class 2
2		c1 7814	. . 3 class 1
3		caddc 7816	. . 3 class +
4	2, 2, 3	co 5877	. 2 class ( 1 + 1 )
5	1, 4	wceq 1353	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8991  0le2  9011  2pos  9012  1p1e2  9038  2p2e4  9048  2times  9049  3p2e5  9062  4p2e6  9064  5p2e7  9067  6p2e8  9070  7p2e9  9072  2nn  9082  1lt2  9090  nneoor  9357  6p6e12  9459  7p5e12  9462  8p2e10  9465  8p4e12  9467  9p2e11  9472  9p3e12  9473  5t2e10  9485  eluz2b1  9603  nn01to3  9619  fztp  10080  fzprval  10084  fztpval  10085  fzo12sn  10219  rebtwn2zlemstep  10255  rebtwn2z  10257  sqval  10580  fac2  10713  bcp1m1  10747  hashprg  10790  binom11  11496  ege2le3  11681  ef4p  11704  efgt1p2  11705  eirraplem  11786  odd2np1lem  11879  opoe  11902  ncoprmgcdne1b  12091  isprm3  12120  prmind2  12122  dvdsnprmd  12127  prmgt1  12134  pockthlem  12356  pockthg  12357  prmunb  12362  mulg2  12997  dveflem  14226  coskpi  14308  lgslem1  14440  lgsval2lem  14450  lgsdir2lem2  14469  lgsdir2lem3  14470  lgsdirprm  14474  m1lgs  14491  ex-fl  14516