Definition df-2

Description: Define the number 2. (Contributed by NM, 27-May-1999)

	Ref	Expression
Assertion	df-2	$$⊢2=1+1$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2	$$class2$$
1		c1	$$class1$$
2		caddc	$$class+$$
3	1 1 2	co	$$class\left(1+1\right)$$
4	0 3	wceq	$$wff2=1+1$$