Theorem addex

Description: The addition operation is a set. (Contributed by NM, 19-Oct-2004) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	addex	$$⊢+\in \mathrm{V}$$

Proof

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