Metamath Proof Explorer

Theorem addex

Description: The addition operation is a set. (Contributed by NM, 19-Oct-2004) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion addex ⊢ + ∈ V

Proof

Step Hyp Ref Expression
1 ax-addf ⊢ + : ℂ × ℂ ⟶ ℂ
2 cnex ⊢ ℂ ∈ V
3 2 2 xpex ⊢ ℂ × ℂ ∈ V
4 fex2 ⊢ + : ℂ × ℂ ⟶ ℂ ∧ ℂ × ℂ ∈ V ∧ ℂ ∈ V → + ∈ V
5 1 3 2 4 mp3an ⊢ + ∈ V