Definition df-2 8937

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 8929	. 2 class 2
2		c1 7775	. . 3 class 1
3		caddc 7777	. . 3 class +
4	2, 2, 3	co 5853	. 2 class ( 1 + 1 )
5	1, 4	wceq 1348	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8948  0le2  8968  2pos  8969  1p1e2  8995  2p2e4  9005  2times  9006  3p2e5  9019  4p2e6  9021  5p2e7  9024  6p2e8  9027  7p2e9  9029  2nn  9039  1lt2  9047  nneoor  9314  6p6e12  9416  7p5e12  9419  8p2e10  9422  8p4e12  9424  9p2e11  9429  9p3e12  9430  5t2e10  9442  eluz2b1  9560  nn01to3  9576  fztp  10034  fzprval  10038  fztpval  10039  fzo12sn  10173  rebtwn2zlemstep  10209  rebtwn2z  10211  sqval  10534  fac2  10665  bcp1m1  10699  hashprg  10743  binom11  11449  ege2le3  11634  ef4p  11657  efgt1p2  11658  eirraplem  11739  odd2np1lem  11831  opoe  11854  ncoprmgcdne1b  12043  isprm3  12072  prmind2  12074  dvdsnprmd  12079  prmgt1  12086  pockthlem  12308  pockthg  12309  prmunb  12314  dveflem  13481  coskpi  13563  lgslem1  13695  lgsval2lem  13705  lgsdir2lem2  13724  lgsdir2lem3  13725  lgsdirprm  13729  ex-fl  13760