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 , y x + y V

Proof

Step Hyp Ref Expression
1 mpoaddf x , y x + y : ×
2 cnex V
3 2 2 xpex × V
4 fex2 x , y x + y : × × V V x , y x + y V
5 1 3 2 4 mp3an x , y x + y V