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	⊢ ( ( · : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ∧ ℂ ∈ V ) → · ∈ V )
5	1 3 2 4	mp3an	⊢ · ∈ V