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	$$⊢\times \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3	2 2	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
4		fex2	$$⊢\left(\times :ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \times \in \mathrm{V}$$
5	1 3 2 4	mp3an	$$⊢\times \in \mathrm{V}$$