Theorem addex 5382

Description: The addition operation is a set.

Assertion

Ref	Expression
addex	|- + e. V

Proof of Theorem addex

Step	Hyp	Ref	Expression
1		axaddopr 5330	. 2 |- + :(CC X. CC)-->CC
2		axcnex 5332	. . 3 |- CC e. V
3	2, 2	xpex 3317	. 2 |- (CC X. CC) e. V
4		fex 3709	. 2 |- (( + :(CC X. CC)-->CC /\ (CC X. CC) e. V) -> + e. V)
5	1, 3, 4	mp2an 709	1 |- + e. V

Syntax hints:   e. wcel 999  Vcvv 1858   X. cxp 3225  -->wf 3235  CCcc 5297   + caddc 5302

This theorem is referenced by:  ser1f 6587  ser1cl1i 6589  ser1recli 6590  ser1refi 6591  ser1f2i 6593  ser11i 6594  ser1p1i 6595  ser1monoi 6596  ser1add2i 6597  ser1addi 6598  serzcl1i 6651  ser0cl1i 6653  ser0fi 6654  ser00i 6655  ser0p1i 6656  ser1absdiflem 7019  sumeq2 7075  fsumserz 7089  fsumser0fi 7091  fsumser1fi 7092  serzfsum 7094  fsum1i 7095  fsump1i 7096  ser0cl 7136  ser1cl 7137  ser1ser0i 7138  serzrefi 7141  ser0mulci 7149  ser1mulci 7150  serzrelem 7151  ser0cji 7155  iserzshfti 7234  clim2serzi 7235  serzf0i 7259  ser1f0i 7260  ser1consti 7261  ser1cmpi 7264  ser1cmp2i 7267  cvgcmp2clem 7272  isumval 7282  isum1clim 7287  isumnn0nn 7297  isum0spliti 7307  geolim1i 7328  geosumi 7331  geoisum 7332  geoisum1 7334  geoisum1c 7335  dfef2i 7397  ef0lem 7400  efseq0ex 7401  efcl 7402  efcvg 7404  efcvgfsum 7405  reefcli 7407  erelem2 7410  erelem6 7414  ege2lem2 7418  ege2le3lem2 7419  efcji 7426  eftlexiOLD 7467  ef1tllem 7471  eirrlem4 7482  effsumlei 7488  efge1i 7492  efge1pi 7493  efm1limi 7502  eflegeolem2 7505  cnnvg 8392  cnnvs 8395  cnph 8562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-plp 5153  df-ltp 5155  df-plpr 5229  df-enr 5231  df-nr 5232  df-plr 5233  df-c 5305  df-plus 5310

Copyright terms: Public domain