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 ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥𝑦 ) = ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )
2 sn-subcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥𝑦 ) ∈ ℂ )
3 1 2 eqeltrrd ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ )
4 3 rgen2 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ
5 df-sub − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) )
6 5 fmpo ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑧 ∈ ℂ ( 𝑦 + 𝑧 ) = 𝑥 ) ∈ ℂ ↔ − : ( ℂ × ℂ ) ⟶ ℂ )
7 4 6 mpbi − : ( ℂ × ℂ ) ⟶ ℂ