Description: The multiplication operation is a set. (Contributed by NM, 19-Oct-2004) (Revised by Mario Carneiro, 17-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mulex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-mulf | |
|
2 | cnex | |
|
3 | 2 2 | xpex | |
4 | fex2 | |
|
5 | 1 3 2 4 | mp3an | |