subf

Description: Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007) (Revised by Mario Carneiro, 16-Nov-2013)

		Ref	Expression
	Assertion	subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$

Step	Hyp	Ref	Expression
1		subval	$⊢ (x \in ℂ \land y \in ℂ) \to x - y = (ι z \in ℂ \| y + z = x)$
2		subcl	$⊢ (x \in ℂ \land y \in ℂ) \to x - y \in ℂ$
3	1 2	eqeltrrd	$⊢ (x \in ℂ \land y \in ℂ) \to (ι z \in ℂ \| y + z = x) \in ℂ$
4	3	rgen2	$⊢ \forall x \in ℂ \forall y \in ℂ (ι z \in ℂ \| y + z = x) \in ℂ$
5		df-sub	$⊢ - = (x \in ℂ, y \in ℂ ⟼ (ι z \in ℂ \| y + z = x))$
6	5	fmpo	$⊢ \forall x \in ℂ \forall y \in ℂ (ι z \in ℂ \| y + z = x) \in ℂ \leftrightarrow - : ℂ \times ℂ ⟶ ℂ$
7	4 6	mpbi	$⊢ - : ℂ \times ℂ ⟶ ℂ$

Metamath Proof Explorer