Definition df-2 7973

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 7964	. 2 class 2
2		c1 6890	. . 3 class 1
3		caddc 6892	. . 3 class +
4	2, 2, 3	co 5512	. 2 class (1 + 1)
5	1, 4	wceq 1243	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  7985  0le2  8006  2pos  8007  1p1e2  8033  2p2e4  8037  2times  8038  3p2e5  8052  4p2e6  8054  5p2e7  8057  6p2e8  8061  7p2e9  8064  8p2e10  8066  2nn  8077  1lt2  8086  nneoor  8340  6p6e12  8418  7p5e12  8420  8p4e12  8424  9p2e11  8429  9p3e12  8430  eluz2b1  8539  nn01to3  8552  fztp  8940  fzprval  8944  fztpval  8945  fzo12sn  9073  rebtwn2zlemstep  9107  rebtwn2z  9109  sqval  9312  ex-fl  9895