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

Metamath Proof Explorer

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 ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = ι z ∈ ℂ | y + z = x
2 sn-subcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y ∈ ℂ
3 1 2 eqeltrrd ⊢ x ∈ ℂ ∧ y ∈ ℂ → ι z ∈ ℂ | y + z = x ∈ ℂ
4 3 rgen2 ⊢ ∀ x ∈ ℂ ∀ y ∈ ℂ ι z ∈ ℂ | y + z = x ∈ ℂ
5 df-sub ⊢ − = x ∈ ℂ , y ∈ ℂ ⟼ ι z ∈ ℂ | y + z = x
6 5 fmpo ⊢ ∀ x ∈ ℂ ∀ y ∈ ℂ ι z ∈ ℂ | y + z = x ∈ ℂ ↔ − : ℂ × ℂ ⟶ ℂ
7 4 6 mpbi ⊢ − : ℂ × ℂ ⟶ ℂ