Definition df-2 8912

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 8904	. 2 class 2
2		c1 7750	. . 3 class 1
3		caddc 7752	. . 3 class +
4	2, 2, 3	co 5841	. 2 class ( 1 + 1 )
5	1, 4	wceq 1343	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8923  0le2  8943  2pos  8944  1p1e2  8970  2p2e4  8980  2times  8981  3p2e5  8994  4p2e6  8996  5p2e7  8999  6p2e8  9002  7p2e9  9004  2nn  9014  1lt2  9022  nneoor  9289  6p6e12  9391  7p5e12  9394  8p2e10  9397  8p4e12  9399  9p2e11  9404  9p3e12  9405  5t2e10  9417  eluz2b1  9535  nn01to3  9551  fztp  10009  fzprval  10013  fztpval  10014  fzo12sn  10148  rebtwn2zlemstep  10184  rebtwn2z  10186  sqval  10509  fac2  10640  bcp1m1  10674  hashprg  10717  binom11  11423  ege2le3  11608  ef4p  11631  efgt1p2  11632  eirraplem  11713  odd2np1lem  11805  opoe  11828  ncoprmgcdne1b  12017  isprm3  12046  prmind2  12048  dvdsnprmd  12053  prmgt1  12060  pockthlem  12282  pockthg  12283  prmunb  12288  dveflem  13287  coskpi  13369  lgslem1  13501  lgsval2lem  13511  lgsdir2lem2  13530  lgsdir2lem3  13531  lgsdirprm  13535  ex-fl  13566