Theorem sn-subf

Description: subf without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ

Proof

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