Metamath Proof Explorer

Theorem mulex

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

Ref Expression
Assertion mulex 
|- x. e. _V

Proof

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