Theorem oprex 3983

Description: The result of an operation is a set.

Assertion

Ref	Expression
oprex	|- (AFB) e. V

Proof of Theorem oprex

Step	Hyp	Ref	Expression
1		df-opr 3965	. 2 |- (AFB) = (F` <.A, B>.)
2		fvex 3732	. 2 |- (F` <.A, B>.) e. V
3	1, 2	eqeltr 1544	1 |- (AFB) e. V

Syntax hints:   e. wcel 958  Vcvv 1811  <.cop 2411  ` cfv 3182  (class class class)co 3963

This theorem is referenced by:  oprvalelrn 4039  ndmoprass 4048  ndmoprdistr 4049  ndmord 4050  ndmordi 4051  caopr4 4064  caopr411 4065  caoprdistrr 4067  caoprdilem 4068  caoprlem2 4069  curry1 4098  curry1val 4100  oasuc 4163  omsuc 4165  oesuc 4166  oacl 4170  omcl 4171  oecl 4172  oaordi 4180  oaass 4195  odi 4210  omass 4211  oneo 4212  brecop2 4307  ecopoprtrn 4311  th3qlem1 4314  mapsnen 4429  map1 4430  mapen 4491  mapdom1 4492  mapdom2 4494  mapxpen 4495  xpmapenlem5 4500  mapunen 4502  pwen 4503  unfilem2 4549  unfilem3 4550  aleph1 4871  mapcdaen 4932  cdainf 4937  addcmpblnq 5052  ordpipq 5056  addcompq 5062  addasspq 5063  distrpq 5067  recmulpq 5070  ltsopq 5075  ltapq 5076  ltmpq 5077  1lt2pq 5078  ltaddpq 5079  ltexpq 5080  halfpq 5082  ltbtwnpq 5084  ltrpq 5085  genpprecl 5104  genpn0 5106  genpnnp 5108  genpnmax 5110  genpass 5112  1pr 5117  addclprlem1 5118  addclprlem2 5119  mulclprlem 5121  distrlem1pr 5127  distrlem4pr 5130  distrlem5pr 5131  1idpr 5133  prlem934a 5137  prlem934b 5138  prlem934 5139  ltexprlem4 5145  ltexprlem7 5148  ltapr 5151  prlem936a 5153  prlem936 5155  reclem3pr 5158  reclem4pr 5159  mulcmpblnrlem 5182  mulcmpblnr 5183  ltsrpr 5186  mulcomsr 5198  distrsr 5200  m1m1sr 5202  ltsosr 5203  0lt1sr 5204  1idsr 5207  ltasr 5209  pn0sr 5210  negexsr 5211  recexsrlem 5212  addgt0sr 5213  mulgt0sr 5214  sqgt0sr 5215  recexsr 5216  ssgt0sr 5217  mappsrpr 5218  ltpsrpr 5219  map2psrpr 5220  supsrlem1 5225  supsrlem2 5226  supsrlem3 5227  supsrlem6 5230  axmulcom 5276  axmulass 5278  axdistr 5279  axrnegex 5283  axrrecex 5284  pre-axltadd 5289  pre-axmulgt0 5290  negex 5365  peano2nn 5935  nn1suc 5939  sup2 6051  nnunb 6070  dfuz 6202  uzindOLD 6208  elq 6257  om2uzsuc 6296  seq1lem1 6309  seq1suclem 6316  2shft 6352  shftcan2t 6353  seq1shftid 6356  ioof 6400  icoshftf1oi 6409  uzind4s 6452  fzrevralt 6519  fzshftralt 6522  seq0fval 6535  seqzfval 6537  seqzfn 6539  seq1seqz 6541  seq1seq02t 6543  seq1seq0t 6544  seq1seq0 6545  seq0fn 6546  seqz1 6547  seqzp1 6548  seq00 6550  seq0p1 6551  seqzval2t 6553  dfseq0 6563  cjvalt 6763  facp1t 6936  bcvalt 6958  sumeq2 6985  fsump1slem 7012  fsump1s 7013  fsumadd 7022  csbfsumlem 7026  csbfsum 7027  fsumcom 7028  fsumrev 7029  fsumshft 7031  fsummulc1 7033  fsumconst 7038  fsumcmp 7040  fsumabs 7043  serzsplit 7056  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem5 7070  binomlem6 7071  bcxmas 7076  climshft 7104  climshft2 7106  iserzshft2 7107  climsub 7130  clim2serzt 7134  iserzext 7135  iserzmulc1 7136  climcmplem 7137  iserzcmp 7142  iserzshft 7144  clim2serz 7145  iserzex 7146  climserzle 7147  caucvg3a 7164  caucvg3lem 7166  caucvg3 7167  iserzabslem 7178  cvgcmp2lem 7180  cvgcmp2 7181  cvgcmp2clem 7182  cvgcmp2c 7183  cvgcmp3ce 7187  isumshft 7204  isumshft2 7205  isum1p 7206  isummulc1 7212  isummulc1ALT 7213  isumsplit 7216  infcvg 7224  fnsmnt 7226  geoser 7234  geolimilem 7235  geolimi 7236  geolim1i 7238  geosum 7241  geoisum 7242  geoisum1 7244  geoisum1c 7245  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  efcltlem1 7304  dfef2 7307  ef0lem 7310  efseq0ex 7311  efclt 7312  efcvg 7314  efcvgfsum 7315  eftval 7316  erelem2 7320  erelem3 7321  erelem6 7324  ege2lem2 7328  ege2le3lem2 7329  efcj 7336  efaddlem5 7342  efaddlem26 7363  efaddlem27 7364  efaddlem28 7365  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  absefm1le 7412  eflegeolem2 7414  sinvalt 7429  cosvalt 7430  sinf 7440  cosf 7441  acdc3 7487  acdc2lem1 7488  acdc2lem2 7489  acdc2 7490  acdc5lem1 7491  acdc5lem2 7492  acdc5 7493  acdc 7495  qnnen 7503  ruclem13 7522  ruclem16 7525  ruclem18 7527  ruclem19 7528  ruclem20 7529  ruclem21 7530  ruclem25 7534  infmap1 7573  infmap2lem2 7580  infmap2 7581  alephadd 7582  alephexp2 7586  cnfval 7756  cnpval 7759  fsumcnlem 7989  grpdivval 8082  grplactval 8097  grplactf1o 8098  sqcn 8335  va1cnlem 8345  sm1cnilem 8347  ipval 8353  ipval2 8357  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem4 8376  ip1cnilem6 8378  nmofval 8425  bloval 8441  ajfval 8469  hmoval 8470  ipasslem6 8495  ipasslem8 8497  ipasslem9 8498  ipblnfi 8516  ubthi 8544  minveclem23 8567  minveclem33 8577  htthlem4 8623  sincolem 8665  shftefif1olem 8741  hvsubvalt 8886  hhip 9044  hsn0elch 9120  occllem3 9175  occllem7 9179  shintcl 9293  hosvalt 9516  hosvaltOLD 9517  homvalt 9518  hodvalt 9519  hodvaltOLD 9520  hfsvalt 9521  hfmvalt 9522  hmopex 9802  bravalvalt 9868  kbvalvalt 9878  eigvalt 9884  cnlnadjlem1 10000  kbass2t 10050  kbass5t 10053  strlem2 10178  elgiso 10398  cdrci 10494  hmeogrp 10538  clicls 10622  stoi 10639

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-uni 2504  df-fv 3198  df-opr 3965

Copyright terms: Public domain