HomeRelated theorems
Unicode version
| Home |
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 5237 |
. 2
      | |
| 2 | axcnex 5239 |
. . 3
| |
| 3 | 2, 2 | xpex 3250 |
. 2
|
| 4 | fex 3637 |
. 2
  | |
| 5 | 1, 3, 4 | mp2an 695 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wcel 955 cvv 1802 cxp 3158 wf 3168 cc 5204 caddc 5209 |
| This theorem is referenced by: ser1ft 6265 ser1cl1 6267 ser1recl 6268 ser1ref 6269 ser1f2 6271 ser11 6272 ser1p1 6273 ser1mono 6274 ser1add2 6275 ser1add 6276 serzcl1 6494 ser0cl1 6496 ser0f 6497 ser00 6498 ser0p1 6499 ser1absdiflem 6866 sumeq2 6923 fsumserz 6937 fsumser0f 6939 fsumser1f 6940 serzfsum 6942 fsum1 6943 fsump1 6944 ser0clt 6984 ser1clt 6985 ser1ser0 6986 serzref 6989 ser0mulc 6997 ser1mulc 6998 serzrelem 6999 ser0cj 7003 iserzshft 7080 clim2serz 7081 serzf0 7105 ser1f0 7106 ser1const 7107 ser1cmp 7110 ser1cmp2 7113 cvgcmp2clem 7118 isumvalt 7128 isumnn0nn 7142 isum0split 7152 geolim1i 7173 geosum 7176 geoisum 7177 geoisum1 7179 geoisum1c 7180 dfef2 7249 ef0lem 7252 efseq0ex 7253 efclt 7254 efcvg 7256 efcvgfsum 7257 reefcl 7259 erelem2 7262 erelem6 7266 ege2lem2 7270 ege2le3lem2 7271 efcj 7278 eftlexOLD 7319 ef1tllem 7323 eirrlem4 7333 effsumle 7338 efge1 7342 efge1p 7343 efm1lim 7351 eflegeolem2 7354 cnnvg 8246 cnnvs 8249 cnph 8409 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-plp 5060 df-ltp 5062 df-plpr 5136 df-enr 5138 df-nr 5139 df-plr 5140 df-c 5212 df-plus 5217 |