Definition df-0

Description: Define the complex number 0. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-0	⊢ 0 = ⟨ 0R , 0R ⟩

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cc0	⊢ 0
1		c0r	⊢ 0R
2	1 1	cop	⊢ ⟨ 0R , 0R ⟩
3	0 2	wceq	⊢ 0 = ⟨ 0R , 0R ⟩