Theorem 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 ℂ⟶ℂ$$

Proof

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