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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoaddf | ||
2 | cnex | ||
3 | 2 2 | xpex | |
4 | fex2 | ||
5 | 1 3 2 4 | mp3an |