Metamath Proof Explorer

Theorem mpoaddex

Description: The addition operation is a set. Version of addex using maps-to notation , which does not require ax-addf . (Contributed by GG, 31-Mar-2025)

		Ref	Expression
	Assertion	mpoaddex	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) \in V$

Proof

Step	Hyp	Ref	Expression
1		mpoaddf	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) : ℂ \times ℂ ⟶ ℂ$
2		cnex	$⊢ ℂ \in V$
3	2 2	xpex	$⊢ ℂ \times ℂ \in V$
4		fex2	$⊢ ((x \in ℂ, y \in ℂ ⟼ x + y) : ℂ \times ℂ ⟶ ℂ \land ℂ \times ℂ \in V \land ℂ \in V) \to (x \in ℂ, y \in ℂ ⟼ x + y) \in V$
5	1 3 2 4	mp3an	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) \in V$