Theorem oprex 4907

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 4886	. 2 |- (AFB) = (F` <.A, B>.)
2		fvex 4689	. 2 |- (F` <.A, B>.) e. _V
3	1, 2	eqeltri 1967	1 |- (AFB) e. _V

Syntax hints:   e. wcel 1300  _Vcvv 2292  <.cop 3046  ` cfv 3998  (class class class)co 4884

This theorem is referenced by:  oprvelrn 4969  ndmoprass 4981  ndmoprdistr 4982  ndmord 4983  ndmordi 4984  caopr4 4997  caopr411 4998  caoprdistrr 5000  caoprdilem 5001  caoprlem2 5002  curry1 5075  curry1val 5077  curry2 5078  curry2val 5080  onopruni 5117  onopriun 5118  oasuc 5208  omsuc 5210  oesuc 5211  oacl 5215  omcl 5216  omclOLD 5217  oecl 5218  oeclOLD 5219  oaordi 5227  oaass 5243  odi 5258  omass 5259  oneo 5260  brecop2 5366  ecopoprtrn 5370  th3qlem1 5373  mapsnen 5488  map1 5489  mapen 5585  mapdom1 5586  mapdom2 5588  mapxpen 5589  xpmapenlem5 5594  mapunen 5596  pwen 5597  unfilem2 5642  unfilem3 5643  aleph1 6019  mapcdaen 6082  cdainf 6087  nnacda 6088  nnaun 6089  addcmpblnq 6204  ordpipq 6208  addcompq 6214  addasspq 6215  distrpq 6219  recmulpq 6222  ltsopq 6227  ltapq 6228  ltmpq 6229  1lt2pq 6230  ltaddpq 6231  ltexpq 6232  halfpq 6234  ltbtwnpq 6236  ltrpq 6237  genpprecl 6256  genpn0 6258  genpnnp 6260  genpnmax 6262  genpass 6264  1pr 6269  addclprlem1 6270  addclprlem2 6271  mulclprlem 6273  distrlem1pr 6279  distrlem4pr 6282  distrlem5pr 6283  1idpr 6285  prlem934a 6289  prlem934b 6290  prlem934 6291  ltexprlem4 6297  ltexprlem7 6300  ltapr 6303  prlem936a 6305  prlem936 6307  reclem3pr 6310  reclem4pr 6311  mulcmpblnrlem 6334  mulcmpblnr 6335  ltsrpr 6338  mulcomsr 6350  distrsr 6352  m1m1sr 6354  ltsosr 6355  0lt1sr 6356  1idsr 6359  ltasr 6361  pn0sr 6362  negexsr 6363  recexsrlem 6364  addgt0sr 6365  mulgt0sr 6366  sqgt0sr 6367  recexsr 6368  ssgt0sr 6369  mappsrpr 6370  ltpsrpr 6371  map2psrpr 6372  supsrlem1 6377  supsrlem2 6378  supsrlem3 6379  supsrlem6 6382  axmulcom 6429  axmulass 6431  axdistr 6432  axrnegex 6436  axrrecex 6437  pre-axltadd 6442  pre-axmulgt0 6443  negex 6522  peano2nn 7118  nn1suc 7122  sup2 7260  nnunb 7279  dfuzi 7414  uzindOLD 7420  elq 7437  modval 7501  ioof 7569  icoshftf1oii 7578  uzind4s 7621  fzen 7664  fzrevral 7698  fzshftral 7701  om2uzsuci 7707  cardfz 7719  seq1lem1 7722  seq1suclem 7729  2shfti 7765  shftcan2 7766  seq1shftid 7769  seq0fval 7778  seqzfval 7780  seqzfn 7782  seq1seqz 7784  seq1seq02 7786  seq1seq01 7787  seq1seq0 7788  seq0fn 7789  seqz1 7790  seqzp1 7791  seq00 7793  seq0p1 7794  seqzval2 7796  dfseq0 7806  cjval 8013  facp1 8188  bcval 8210  fz1fi 8229  sumeq2 8245  fsump1slem 8272  fsump1s 8273  fsumadd 8282  csbfsumlem 8286  csbfsum 8287  fsumcom 8288  fsumrev 8289  fsumshft 8291  fsummulc1 8293  fsumconst 8298  fsumcmp 8300  fsumabs 8303  serzsplit 8316  binomlem2 8327  binomlem3 8328  binomlem4 8329  binomlem5 8330  binomlem6 8331  bcxmas 8336  climshfti 8364  climshft2i 8366  iserzshft2i 8367  climsub 8390  clim2serz 8394  iserzex 8395  iserzmulc1 8396  climcmplem 8397  iserzcmp 8402  iserzshfti 8404  clim2serzi 8405  iserzexi 8406  climserzlei 8407  caucvg3ai 8424  caucvg3lem 8426  caucvg3i 8427  iserzabslem 8438  cvgcmp2lem 8440  cvgcmp2i 8441  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  cvgcmp2ci 8444  cvgcmp3cei 8448  isumshfti 8465  isumshft2i 8466  isum1p 8467  isummulc1 8473  isummulc1iALT 8474  isumspliti 8477  infcvgi 8485  arisumi 8487  explecnv 8495  geoseri 8496  geolimilem 8497  geolimi 8498  geolim1i 8500  geosumi 8503  geoisum 8504  geoisum1 8506  geoisum1c 8507  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag 8520  fsum0diag2 8521  fsum0diag4 8523  efcltlem1 8566  dfef2i 8569  ef0lem 8572  efseq0ex 8573  efcl 8574  efcvg 8576  efcvgfsum 8577  eftval 8578  erelem2 8582  erelem3 8583  erelem6 8586  ege2lem2 8590  ege2le3lem2 8591  efcji 8598  efaddlem5 8604  efaddlem26 8625  efaddlem27 8626  efaddlem28 8627  ef1tllem 8643  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  absefm1lei 8677  eflegeolem2 8679  sinval 8694  cosval 8695  sinf 8705  cosf 8706  acdc3 8755  acdc2lem1 8757  acdc2lem2 8758  acdc2 8759  acdc5lem1 8760  acdc5lem2 8761  acdc5 8762  acdc 8764  qnnen 8772  ruclem13 8791  ruclem16 8794  ruclem18 8796  ruclem19 8797  ruclem20 8798  ruclem21 8799  ruclem25 8803  infmap1 8842  infmap2lem2 8849  infmap2 8850  alephadd 8851  alephexp2 8855  cnfval 9032  cnpval 9035  fsumcnlem 9267  grpdivval 9367  grplactval 9405  grplactf1o 9406  gaid 9454  gapm 9462  sqcn 9674  va1cnlem 9684  sm1cnilem 9686  ipval 9692  ipval2 9696  ip1cnilem2 9713  ip1cnilem3 9714  ip1cnilem4 9715  ip1cnilem6 9717  nmofval 9764  bloval 9781  ajfval 9809  hmoval 9810  ipasslem6 9836  ipasslem8 9838  ipasslem9 9839  ipblnfi 9857  ubthi 9889  minveclem23 9912  minveclem33 9922  htthlem4 9970  sincolem 10014  shftefif1olem 10095  cdrci 10182  clicls 10183  subtopmet 10256  filmapf 10307  flimff 10317  hvsubval 10518  hhip 10677  hsn0elch 10753  occllem3 10808  occllem7 10812  shintcli 10926  hosval 11149  hosvalOLD 11150  homval 11151  hodval 11152  hodvalOLD 11153  hfsval 11154  hfmval 11155  hmopex 11439  bravalval 11505  kbvalval 11515  eigval1 11521  cnlnadjlem1 11637  kbass2 11688  kbass5 11691  opsqrlem4 11714  strlem2 11823  fseq1cl 13619  elgiso 13639  eucalglt 13753  mulgcdlem2 13757  mulgcdlem4 13759  cmpdom2 14482  valvalcurfn 14554  nfwval 14588  gepsup 14593  seinf 14594  prodeq2 14661  fprodp1slem 14681  fprodp1s 14682  fprod1ib 14686  fincmpzer 14711  fprodadd 14713  expm 14725  curgrpact 14735  fprodneg 14741  trdom2 14755  trooo 14758  trinv 14759  cmprtr 14760  prsubrtr 14763  svli2 14826  hmeogrp 14892  trhom 14983  stoi 14998  cntrsetlem 14999  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualded 15132  idsubfun 15206  reconnlem1 15446  eropreu 15733  sdclem2 15810  sdc 15811  fdc 15812  fsum00 15820  fsumltisumi 15823  fsumlt1 15831  metf1o 15843  mettrifi2 15848  geomcau 15849  lmclim2 15850  metdcn 15853  icoopnst 15876  iocopnst 15877  addccncf 15883  sub1cncf 15885  sub2cncf 15886  sstotbnd 15936  totbndss 15937  totbndbnd 15944  heiborlem1 15955  heiborlem28 15982  heiborlem29 15983  bfplem8 16005  rrnval 16013  rrndm 16015  rrnmet 16016  rrndstprj1 16017  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  ismrer1 16024  phtpyfval 16046  phtpyval 16047  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpcval 16058  reparphtlem2 16064  pcofval 16072  pcoval 16073  pcocn 16076  pcoloopf 16079  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1bval 16088  pi1fval 16092  pi1gp 16095  rngisoval 16131  iscringd 16147  0idl 16173  intidl 16177  isfldidl 16216  isdmn3 16222  addrfv 16469  subrfv 16470  mulvfv 16471  addrfn 16472  subrfn 16473  mulvfn 16474  elstr 16714  elstrdiff 16720  eustrdif 16722  joinlem 16817  meetlem 16824  hlrelat5 17050  pautset 17395

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-sep 3438  ax-nul 3445  ax-pow 3481  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-uni 3178  df-fv 4014  df-opr 4886

Copyright terms: Public domain