Description: subf without ax-mulcom . (Contributed by SN, 5-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | sn-subf | ⊢ − : ( ℂ × ℂ ) ⟶ ℂ |
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 | ⊢ − : ( ℂ × ℂ ) ⟶ ℂ |