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

Proof

Step Hyp Ref Expression
1 ax-mulf ×:×
2 cnex V
3 2 2 xpex ×V
4 fex2 ×:××VV×V
5 1 3 2 4 mp3an ×V