Metamath Proof Explorer


Theorem mpoaddex

Description: The addition operation is a set. Version of addex using maps-to notation , which does not require ax-addf . (Contributed by GG, 31-Mar-2025)

Ref Expression
Assertion mpoaddex ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ∈ V

Proof

Step Hyp Ref Expression
1 mpoaddf ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ
2 cnex ℂ ∈ V
3 2 2 xpex ( ℂ × ℂ ) ∈ V
4 fex2 ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ∧ ℂ ∈ V ) → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ∈ V )
5 1 3 2 4 mp3an ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ∈ V