| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The addition operation is a set. |
| Ref | Expression |
|---|---|
| addex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axaddopr 6417 |
. 2
| |
| 2 | axcnex 6419 |
. . 3
| |
| 3 | 2, 2 | xpex 4096 |
. 2
|
| 4 | fex 4595 |
. 2
| |
| 5 | 1, 3, 4 | mp2an 761 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: ser1f 7741 ser1cl1i 7743 ser1recli 7744 ser1refi 7745 ser1f2i 7747 ser11i 7748 ser1p1i 7749 ser1monoi 7750 ser1add2i 7751 ser1addi 7752 serzcl1i 7805 ser0cl1i 7807 ser0fi 7808 ser00i 7809 ser0p1i 7810 ser1absdiflem 8181 sumeq2 8245 fsumserz 8259 fsumser0fi 8261 fsumser1fi 8262 serzfsum 8264 fsum1i 8265 fsump1i 8266 ser0cl 8306 ser1cl 8307 ser1ser0i 8308 serzrefi 8311 ser0mulci 8319 ser1mulci 8320 serzrelem 8321 ser0cji 8325 iserzshfti 8404 clim2serzi 8405 serzf0i 8429 ser1f0i 8430 ser1consti 8431 ser1cmpi 8434 ser1cmp2i 8437 cvgcmp2clem 8442 cvgcmp2clemOLD 8443 isumval 8453 isum1clim 8458 isumnn0nn 8468 isum0spliti 8478 geolim1i 8500 geosumi 8503 geoisum 8504 geoisum1 8506 geoisum1c 8507 dfef2i 8569 ef0lem 8572 efseq0ex 8573 efcl 8574 efcvg 8576 efcvgfsum 8577 reefcli 8579 erelem2 8582 erelem6 8586 ege2lem2 8590 ege2le3lem2 8591 efcji 8598 eftlexiOLD 8639 ef1tllem 8643 eirrlem4 8654 effsumlei 8662 efge1i 8666 efge1pi 8667 efm1limi 8676 eflegeolem2 8679 cnnvg 9640 cnnvs 9643 cnph 9819 fprod1s1 14679 fprodp1s1 14683 fprod1i2 14685 zintdom 14787 cntrsetlem 14999 fsumltisumi 15823 geomcau 15849 cnaddablNEW 17139 cnaddablxNEW 17140 zaddablxNEW 17141 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-plp 6240 df-ltp 6242 df-plpr 6316 df-enr 6318 df-nr 6319 df-plr 6320 df-c 6392 df-plus 6397 |