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 
|- + e. _V

Proof

Step Hyp Ref Expression
1 ax-addf 
 |-  + : ( CC X. CC ) --> CC
2 cnex 
 |-  CC e. _V
3 2 2 xpex 
 |-  ( CC X. CC ) e. _V
4 fex2 
 |-  ( ( + : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V /\ CC e. _V ) -> + e. _V )
5 1 3 2 4 mp3an 
 |-  + e. _V