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	⊢ + ∈ V

Proof

Step	Hyp	Ref	Expression
1		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
2		cnex	⊢ ℂ ∈ V
3	2 2	xpex	⊢ ( ℂ × ℂ ) ∈ V
4		fex2	⊢ ( ( + : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ∧ ℂ ∈ V ) → + ∈ V )
5	1 3 2 4	mp3an	⊢ + ∈ V