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=⟨0_{𝑹},0_{𝑹}⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cc0	$$class0$$
1		c0r	$$class{0}_{𝑹}$$
2	1 1	cop	$$class⟨0_{𝑹},0_{𝑹}⟩$$
3	0 2	wceq	$$wff0=⟨0_{𝑹},0_{𝑹}⟩$$