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 |
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 |