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