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 4428  map1 4429  mapen 4489  mapdom1 4490  mapdom2 4492  mapxpen 4493  xpmapenlem5 4498  mapunen 4500  pwen 4501  unfilem2 4544  unfilem3 4545  aleph1 4863  mapcdaen 4924  cdainf 4929  addcmpblnq 5044  ordpipq 5048  addcompq 5054  addasspq 5055  distrpq 5059  recmulpq 5062  ltsopq 5067  ltapq 5068  ltmpq 5069  1lt2pq 5070  ltaddpq 5071  ltexpq 5072  halfpq 5074  ltbtwnpq 5076  ltrpq 5077  genpprecl 5096  genpn0 5098  genpnnp 5100  genpnmax 5102  genpass 5104  1pr 5109  addclprlem1 5110  addclprlem2 5111  mulclprlem 5113  distrlem1pr 5119  distrlem4pr 5122  distrlem5pr 5123  1idpr 5125  prlem934a 5129  prlem934b 5130  prlem934 5131  ltexprlem4 5137  ltexprlem7 5140  ltapr 5143  prlem936a 5145  prlem936 5147  reclem3pr 5150  reclem4pr 5151  mulcmpblnrlem 5174  mulcmpblnr 5175  ltsrpr 5178  mulcomsr 5190  distrsr 5192  m1m1sr 5194  ltsosr 5195  0lt1sr 5196  1idsr 5199  ltasr 5201  pn0sr 5202  negexsr 5203  recexsrlem 5204  addgt0sr 5205  mulgt0sr 5206  sqgt0sr 5207  recexsr 5208  ssgt0sr 5209  mappsrpr 5210  ltpsrpr 5211  map2psrpr 5212  supsrlem1 5217  supsrlem2 5218  supsrlem3 5219  supsrlem6 5222  axmulcom 5268  axmulass 5270  axdistr 5271  axrnegex 5275  axrrecex 5276  pre-axltadd 5281  pre-axmulgt0 5282  negex 5357  peano2nn 5923  nn1suc 5927  sup2 6039  nnunb 6058  dfuz 6190  uzindOLD 6196  elq 6243  om2uzsuc 6282  seq1lem1 6295  seq1suclem 6302  2shft 6338  shftcan2t 6339  seq1shftid 6342  ioof 6386  icoshftf1oi 6395  uzind4s 6438  fzrevralt 6505  fzshftralt 6508  seq0fval 6521  seqzfval 6523  seqzfn 6525  seq1seqz 6527  seq1seq02t 6529  seq1seq0t 6530  seq1seq0 6531  seq0fn 6532  seqz1 6533  seqzp1 6534  seq00 6536  seq0p1 6537  seqzval2t 6539  dfseq0 6549  cjvalt 6749  facp1t 6921  bcvalt 6943  sumeq2 6970  fsump1slem 6997  fsump1s 6998  fsumadd 7007  csbfsumlem 7011  csbfsum 7012  fsumcom 7013  fsumrev 7014  fsumshft 7016  fsummulc1 7018  fsumconst 7023  fsumcmp 7025  fsumabs 7028  serzsplit 7041  binomlem2 7052  binomlem3 7053  binomlem4 7054  binomlem5 7055  binomlem6 7056  bcxmas 7061  climshft 7089  climshft2 7091  iserzshft2 7092  climsub 7115  clim2serzt 7119  iserzext 7120  iserzmulc1 7121  climcmplem 7122  iserzcmp 7127  iserzshft 7129  clim2serz 7130  iserzex 7131  climserzle 7132  caucvg3a 7149  caucvg3lem 7151  caucvg3 7152  iserzabslem 7163  cvgcmp2lem 7165  cvgcmp2 7166  cvgcmp2clem 7167  cvgcmp2c 7168  cvgcmp3ce 7172  isumshft 7189  isumshft2 7190  isum1p 7191  isummulc1 7197  isummulc1ALT 7198  isumsplit 7201  infcvg 7209  fnsmnt 7211  geoser 7219  geolimilem 7220  geolimi 7221  geolim1i 7223  geosum 7226  geoisum 7227  geoisum1 7229  geoisum1c 7230  cvgratlem5 7239  fsum0diaglem2 7242  fsum0diag 7243  fsum0diag2 7244  fsum0diag4 7246  efcltlem1 7289  dfef2 7292  ef0lem 7295  efseq0ex 7296  efclt 7297  efcvg 7299  efcvgfsum 7300  eftval 7301  erelem2 7305  erelem3 7306  erelem6 7309  ege2lem2 7313  ege2le3lem2 7314  efcj 7321  efaddlem5 7327  efaddlem26 7348  efaddlem27 7349  efaddlem28 7350  ef1tllem 7366  ef01tllem1 7368  ef01tllem2 7369  ef01tllem2OLD 7370  absefm1le 7397  eflegeolem2 7399  sinvalt 7414  cosvalt 7415  sinf 7425  cosf 7426  acdc3 7472  acdc2lem1 7473  acdc2lem2 7474  acdc2 7475  acdc5lem1 7476  acdc5lem2 7477  acdc5 7478  acdc 7480  qnnen 7488  ruclem13 7507  ruclem16 7510  ruclem18 7512  ruclem19 7513  ruclem20 7514  ruclem21 7515  ruclem25 7519  infmap1 7558  infmap2lem2 7565  infmap2 7566  alephadd 7567  alephexp2 7571  cnfval 7741  cnpval 7744  fsumcnlem 7974  grpdivval 8067  grplactval 8082  grplactf1o 8083  sqcn 8320  va1cnlem 8330  sm1cnilem 8332  ipval 8338  ipval2 8342  ip1cnilem2 8359  ip1cnilem3 8360  ip1cnilem4 8361  ip1cnilem6 8363  nmofval 8410  bloval 8426  ajfval 8454  hmoval 8455  ipasslem6 8480  ipasslem8 8482  ipasslem9 8483  ipblnfi 8501  ubthi 8529  minveclem23 8552  minveclem33 8562  htthlem4 8608  sincolem 8650  shftefif1olem 8726  hvsubvalt 8871  hhip 9029  hsn0elch 9105  occllem3 9160  occllem7 9164  shintcl 9278  hosvalt 9501  hosvaltOLD 9502  homvalt 9503  hodvalt 9504  hodvaltOLD 9505  hfsvalt 9506  hfmvalt 9507  hmopex 9787  bravalvalt 9853  kbvalvalt 9863  eigvalt 9869  cnlnadjlem1 9985  kbass2t 10035  kbass5t 10038  strlem2 10163  elgiso 10383  cdrci 10466  hmeogrp 10510  clicls 10565  stoi 10582

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