This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-1

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

		Ref	Expression
	Assertion	df-1	$⊢ 1 = ⟨1_{𝑹}, 0_{𝑹}⟩$

Step	Hyp	Ref	Expression
0		c1	$class 1$
1		c1r	$class 1_{𝑹}$
2		c0r	$class 0_{𝑹}$
3	1 2	cop	$class ⟨1_{𝑹}, 0_{𝑹}⟩$
4	0 3	wceq	$wff 1 = ⟨1_{𝑹}, 0_{𝑹}⟩$