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 e. CC , y e. CC |-> ( x + y ) ) e. _V

Proof

Step	Hyp	Ref	Expression
1		mpoaddf	|- ( x e. CC , y e. CC |-> ( x + y ) ) : ( CC X. CC ) --> CC
2		cnex	|- CC e. _V
3	2 2	xpex	|- ( CC X. CC ) e. _V
4		fex2	|- ( ( ( x e. CC , y e. CC |-> ( x + y ) ) : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V /\ CC e. _V ) -> ( x e. CC , y e. CC |-> ( x + y ) ) e. _V )
5	1 3 2 4	mp3an	|- ( x e. CC , y e. CC |-> ( x + y ) ) e. _V