Definition df-2 7753

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 7744	. 2 class 2
2		c1 6712	. . 3 class 1
3		caddc 6714	. . 3 class +
4	2, 2, 3	co 5455	. 2 class (1 + 1)
5	1, 4	wceq 1242	1 wff 2 = (1 + 1)

This definition is referenced by:  2re  7765  0le2  7786  2pos  7787  1p1e2  7811  2p2e4  7815  2times  7816  3p2e5  7830  4p2e6  7832  5p2e7  7835  6p2e8  7839  7p2e9  7842  8p2e10  7844  2nn  7855  1lt2  7864  nneoor  8116  6p6e12  8194  7p5e12  8196  8p4e12  8200  9p2e11  8205  9p3e12  8206  eluz2b1  8315  nn01to3  8328  fztp  8710  fzprval  8714  fztpval  8715  fzo12sn  8843  sqval  8966