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	⊢ − : ( ℂ × ℂ ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		subval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )
2		subcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) ∈ ℂ )
3	1 2	eqeltrrd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ )
4	3	rgen2	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ
5		df-sub	⊢ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )
6	5	fmpo	⊢ ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ℩ 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ ↔ − : ( ℂ × ℂ ) ⟶ ℂ )
7	4 6	mpbi	⊢ − : ( ℂ × ℂ ) ⟶ ℂ