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	⊢ 2
1		c1	⊢ 1
2		caddc	⊢ +
3	1 1 2	co	⊢ ( 1 + 1 )
4	0 3	wceq	⊢ 2 = ( 1 + 1 )