This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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