Definition df-2 9192

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 9184	. 2 class 2
2		c1 8023	. . 3 class 1
3		caddc 8025	. . 3 class +
4	2, 2, 3	co 6013	. 2 class (1 + 1)
5	1, 4	wceq 1395	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  9203  0le2  9223  2pos  9224  1p1e2  9250  2p2e4  9260  2times  9261  3p2e5  9275  4p2e6  9277  5p2e7  9280  6p2e8  9283  7p2e9  9285  2nn  9295  1lt2  9303  nneoor  9572  6p6e12  9674  7p5e12  9677  8p2e10  9680  8p4e12  9682  9p2e11  9687  9p3e12  9688  5t2e10  9700  eluz2b1  9825  nn01to3  9841  fztp  10303  fzprval  10307  fztpval  10308  fzo12sn  10452  fzosplitpr  10469  rebtwn2zlemstep  10502  rebtwn2z  10504  sqval  10849  fac2  10983  bcp1m1  11017  hashprg  11062  binom11  12037  ege2le3  12222  ef4p  12245  efgt1p2  12246  eirraplem  12328  odd2np1lem  12423  opoe  12446  bitsfzolem  12505  ncoprmgcdne1b  12651  isprm3  12680  prmind2  12682  dvdsnprmd  12687  prmgt1  12694  pockthlem  12919  pockthg  12920  prmunb  12925  4sqlem19  12972  2expltfac  13002  gsumpr12val  13473  mulg2  13708  dveflem  15440  coskpi  15562  mersenne  15711  perfectlem2  15714  lgslem1  15719  lgsval2lem  15729  lgsdir2lem2  15748  lgsdir2lem3  15749  lgsdirprm  15753  lgseisen  15793  m1lgs  15804  ex-fl  16257