Definition df-2 8579

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 8571	. 2 class 2
2		c1 7448	. . 3 class 1
3		caddc 7450	. . 3 class +
4	2, 2, 3	co 5690	. 2 class ( 1 + 1 )
5	1, 4	wceq 1296	1 wff 2 = ( 1 + 1 )

This definition is referenced by:  2re  8590  0le2  8610  2pos  8611  1p1e2  8637  2p2e4  8641  2times  8642  3p2e5  8655  4p2e6  8657  5p2e7  8660  6p2e8  8663  7p2e9  8665  2nn  8675  1lt2  8683  nneoor  8947  6p6e12  9049  7p5e12  9052  8p2e10  9055  8p4e12  9057  9p2e11  9062  9p3e12  9063  5t2e10  9075  eluz2b1  9187  nn01to3  9201  fztp  9641  fzprval  9645  fztpval  9646  fzo12sn  9777  rebtwn2zlemstep  9813  rebtwn2z  9815  sqval  10128  fac2  10254  bcp1m1  10288  hashprg  10331  binom11  11029  ege2le3  11110  ef4p  11133  efgt1p2  11134  eirraplem  11213  odd2np1lem  11299  opoe  11322  ncoprmgcdne1b  11498  isprm3  11527  prmind2  11529  dvdsnprmd  11534  prmgt1  11540  ex-fl  12360