Theorem ovexd 7422

Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Assertion

Ref	Expression
ovexd	⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Proof of Theorem ovexd

Step	Hyp	Ref	Expression
1		ovex 7420	. 2 ⊢ (𝐴𝐹𝐵) ∈ V
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  caofidlcan  7691  caofass  7693  caofdi  7695  caofdir  7696  caonncan  7697  suppofssd  8182  mapsnend  9007  snmapen  9009  pw2eng  9047  mapen  9105  mapxpen  9107  mapunen  9110  mapdom2  9112  cantnfcl  9620  cantnfle  9624  cantnflt  9625  cantnflt2  9626  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom3lem  9656  fzen  13502  seqf1o  14008  wrdexg  14489  wrdnval  14510  pfxval  14638  pfxswrd  14671  splval  14716  cshwsexaOLD  14790  ofccat  14935  climshftlem  15540  climshft  15542  climshft2  15548  caucvgr  15642  fsumrev  15745  hashdvds  16745  setsabs  17149  ressress  17217  firest  17395  prdsvscafval  17443  qusval  17505  xpsbas  17535  xpsadd  17537  xpsmul  17538  xpssca  17539  xpsvsca  17540  xpsless  17541  xpsle  17542  homfval  17653  comfval  17661  cicfval  17759  rescabs  17795  rescabs2  17796  resscat  17814  funcres2c  17865  ressffth  17902  fucbas  17925  fuccoval  17928  setchom  18042  catchom  18065  catcco  18067  estrchom  18088  funcestrcsetclem5  18105  funcsetcestrclem5  18120  evlf2val  18180  curf11  18187  curf12  18188  curf2val  18191  uncfval  18195  diagval  18201  hof2  18218  yonval  18222  gsumval2a  18612  gsumval2  18613  mndpsuppss  18692  gsumwspan  18773  efmnd  18797  ghmqusnsglem1  19212  ghmqusnsglem2  19213  ghmqusnsg  19214  ghmquskerlem1  19215  ghmquskerco  19216  ghmquskerlem2  19217  ghmquskerlem3  19218  ghmqusker  19219  orbstafun  19243  orbstaval  19244  symgval  19301  psgnvalii  19439  lsmhash  19635  frgpupval  19704  qusabl  19795  gsumval3  19837  gsumreidx  19847  gsumzaddlem  19851  gsummptshft  19866  telgsumfzslem  19918  telgsumfz  19920  telgsumfz0  19922  dpjval  19988  prdsrngd  20085  srgbinomlem3  20137  srgbinomlem4  20138  mulgass3  20262  rngcval  20527  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  ringcval  20556  rhmsscmap2  20567  rhmsscmap  20568  funcringcsetc  20583  srhmsubclem3  20588  srhmsubc  20589  fldhmsubc  20694  lcomfsupp  20808  rmodislmodlem  20835  rmodislmod  20836  sraval  21082  srasca  21087  crngridl  21190  quscrng  21193  rhmqusnsg  21195  pzriprnglem11  21401  znval  21445  znzrhfo  21457  znunithash  21474  cygznlem2  21478  frobrhm  21485  pjfval  21615  pjpm  21617  frlmgsum  21681  frlmipval  21688  frlmphllem  21689  frlmphl  21690  frlmsslsp  21705  frlmup1  21707  gsumbagdiaglem  21839  psrass1lem  21841  rhmpsrlem1  21849  psrass1  21873  psrdi  21874  psrdir  21875  psrass23l  21876  psrascl  21888  mplval  21898  mplsubglem  21908  mplsubrglem  21913  mplmonmul  21943  mplcoe1  21944  opsrval  21953  psrbagev1  21984  psrbagev2  21985  evlslem6  21988  evlslem1  21989  evlsval  21993  mpfconst  22008  mpff  22011  mpfaddcl  22012  mpfmulcl  22013  mpfind  22014  mhpmulcl  22036  mhpaddcl  22038  psdcoef  22047  psdmplcl  22049  psdadd  22050  ply1lss  22081  gsumply1subr  22118  coe1add  22150  coe1tm  22159  coe1tmmul  22163  cply1mul  22183  ply1coe  22185  evl1expd  22232  pf1mpf  22239  pf1ind  22242  mhmcompl  22267  mhmcoaddmpl  22268  rhmmpl  22270  rhmply1vsca  22275  mamufv  22281  mamuass  22289  mamuvs1  22292  mamuvs2  22293  matgsum  22324  dmatmul  22384  scmatval  22391  scmatrhmval  22414  mvmulfv  22431  mavmulfv  22433  mavmulass  22436  marrepeval  22450  marepveval  22455  submaeval  22469  mdetrsca  22490  mdetunilem9  22507  mdetuni0  22508  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  smadiadetlem3  22555  cramerlem1  22574  mat2pmatmul  22618  m2cpminvid  22640  decpmatfsupp  22656  decpmatmullem  22658  decpmatmul  22659  decpmatmulsumfsupp  22660  pmatcollpw1lem1  22661  pmatcollpw3fi1lem1  22673  pmatcollpwscmatlem2  22677  pm2mpfval  22683  pm2mpf  22685  mply1topmatcllem  22690  mp2pm2mplem3  22695  mp2pm2mplem4  22696  pm2mpmhmlem1  22705  pm2mpmhmlem2  22706  pm2mp  22712  chfacfscmulfsupp  22746  chfacfscmulgsum  22747  chfacfpmmulfsupp  22750  chfacfpmmulgsum  22751  cpmidpmatlem3  22759  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cayhamlem4  22775  xpstopnlem2  23698  fcfval  23920  tsmsxplem1  24040  tsmsxplem2  24041  tusval  24153  xpsdsfn  24265  xpsxmet  24268  xpsdsval  24269  xpsmet  24270  tmsval  24369  met1stc  24409  metuval  24437  cnmpopc  24822  pi1val  24937  pi1addf  24947  pi1addval  24948  pi1grplem  24949  rrxnm  25291  rrxcph  25292  rrxmval  25305  mbfmulc2  25564  mbfmul  25627  itg2mulclem  25647  ibladd  25722  itgadd  25726  itgabs  25736  bddmulibl  25740  dvmulf  25846  dvcmulf  25848  dvmptmul  25865  cmvth  25895  dvlip  25898  ftc1lem4  25946  mdegmullem  25983  coe1mul3  26004  r1pval  26063  plyco  26146  dgrcolem1  26179  elqaalem3  26229  taylpfval  26272  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  advlogexp  26564  logtayl  26569  logccv  26572  dvcxp1  26649  dvcncxp1  26652  logbmpt  26698  logbfval  26700  relogbf  26701  dvatan  26845  cxp2lim  26887  cxploglim2  26889  lgamgulmlem2  26940  lgamgulm2  26946  lgamcvglem  26950  lgamf  26952  basellem7  26997  basellem8  26998  basellem9  26999  fsumdvdscom  27095  logexprlim  27136  dchrfi  27166  gausslemma2dlem2  27278  gausslemma2dlem3  27279  2lgslem1b  27303  chtppilimlem2  27385  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  vmadivsum  27393  dchrisum0lem3  27430  mudivsum  27441  logdivsum  27444  log2sumbnd  27455  selberglem1  27456  selberg2lem  27461  selberg2  27462  selbergr  27479  negsval  27931  wlkp1  29609  cyclnumvtx  29730  wwlksnextsurj  29830  wwlksnextbij  29832  clwlkclwwlklem2a1  29921  clwlkclwwlkf1  29939  eupth2eucrct  30146  frgrncvvdeq  30238  numclwlk2lem2fv  30307  numclwwlk2lem3  30309  ofoprabco  32588  fsuppcurry1  32648  fsuppcurry2  32649  offinsupp1  32650  ressprs  32890  resspos  32892  mntoval  32908  mgcoval  32912  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  lmodvslmhm  32990  gsumwrd2dccat  33007  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  conjga  33127  cntrval2  33128  fxpsubm  33129  archirngz  33143  archiabllem2a  33148  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnsubrunlem2  33199  rlocval  33210  fracval  33254  quslmod  33329  quslmhm  33330  quslvec  33331  qustriv  33335  qustrivr  33336  unitprodclb  33360  nsgmgc  33383  nsgqusf1olem1  33384  nsgqusf1olem2  33385  nsgqusf1olem3  33386  lmhmqusker  33388  rhmquskerlem  33396  elrspunidl  33399  qsidomlem1  33423  qsidomlem2  33424  opprqusbas  33459  opprqusplusg  33460  opprqusmulr  33462  opprqus1r  33463  qsdrngilem  33465  qsdrngi  33466  rprmdvdsprod  33505  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  1arithufdlem3  33517  dfufd2lem  33520  zringfrac  33525  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1gsumz  33564  r1plmhm  33575  resssra  33583  ply1degltdimlem  33618  ply1degltdim  33619  qusdimsum  33624  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  lactlmhm  33630  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  algextdeglem4  33710  algextdeglem6  33712  algextdeglem7  33713  submateq  33799  lmatcl  33806  mdetpmtr1  33813  madjusmdetlem1  33817  madjusmdetlem3  33819  qqhvval  33973  esumfzf  34059  esumpfinvallem  34064  esumpmono  34069  esummulc1  34071  esumcvg  34076  esumgect  34080  ofcval  34089  omssubadd  34291  sitgfval  34332  sitmcl  34342  sseqfv2  34385  cndprobval  34424  ballotlemfval  34481  ballotlemsv  34501  ballotlemsf1o  34505  ofcccat  34534  signsplypnf  34541  signsply0  34542  signstfval  34555  signshf  34579  reprpmtf1o  34617  reprdifc  34618  logdivsqrle  34641  hgt750lemg  34645  hgt750lema  34648  lpadval  34667  cvmliftlem8  35279  cvmliftphtlem  35304  fmla1  35374  gonarlem  35381  sategoelfvb  35406  mrsubval  35496  ellcsrspsn  35628  r1peuqusdeg1  35630  fwddifval  36150  knoppcnlem1  36481  knoppcnlem6  36486  unbdqndv2lem2  36498  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem19  37633  poimirlem22  37636  poimirlem23  37637  broucube  37648  dvtan  37664  itg2addnc  37668  ibladdnc  37671  itgaddnc  37674  itgmulc2nclem2  37681  itgmulc2nc  37682  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem3  37689  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  areacirclem1  37702  areacirc  37707  fsumshftd  38945  hlrelat5N  39395  rhmzrhval  41959  aks6d1c1  42104  hashscontpow  42110  aks6d1c4  42112  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem1  42158  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  aks6d1c7lem2  42169  unitscyglem1  42183  readvrec2  42349  readvrec  42350  readvcot  42352  frlmfzolen  42491  frlmfzoccat  42493  frlmvscadiccat  42494  evlscl  42546  evlsval3  42547  evlsvval  42548  evlsvvval  42551  evlsbagval  42554  evlsexpval  42555  evlsaddval  42556  evlsmulval  42557  evlsevl  42559  evlcl  42560  evladdval  42563  evlmulval  42564  selvcl  42571  evlselv  42575  fsuppind  42578  mhpind  42582  mhphflem  42584  prjspner  42607  prjspnvs  42608  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  0prjspnrel  42615  prjcrv0  42621  mzpclall  42715  mzpsubst  42736  eldioph2  42750  rabdiophlem2  42790  irrapxlem1  42810  mzpcong  42961  mendlmod  43178  naddcnff  43351  relexpmulnn  43698  iunrelexpuztr  43708  mnringvald  44202  mnringmulrvald  44216  radcnvrat  44303  hashnzfzclim  44311  lhe4.4ex1a  44318  expgrowthi  44322  expgrowth  44324  bccval  44327  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemradcnv  44341  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  unirnmap  45202  unirnmapsn  45208  ssmapsn  45210  iocopn  45518  icoopn  45523  divcnvg  45625  sumnnodd  45628  climsubmpt  45658  dvsinax  45911  fperdvper  45917  dvdivf  45920  dvnprodlem1  45944  itgsincmulx  45972  stoweidlem59  46057  etransclem4  46236  etransclem13  46245  etransclem25  46257  etransclem48  46280  rrxtopnfi  46285  sge0tsms  46378  elhoi  46540  ovnval2  46543  ovnval2b  46550  ovncvrrp  46562  ovn0lem  46563  ovncl  46565  ovnome  46571  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvle  46598  ovnlecvr2  46608  ovncvr2  46609  ovnsubadd2lem  46643  ovnovollem1  46654  vonvolmbl  46659  iunhoiioolem  46673  vonioolem1  46678  vonioolem2  46679  vonicclem2  46682  smfresal  46786  smfres  46788  smfmullem4  46792  smfco  46800  adddmmbl  46831  muldmmbl  46833  sinnpoly  46892  fmtno  47530  isubgruhgr  47868  grtriprop  47940  grtriclwlk3  47944  gpgvtx  48034  gpgiedg  48035  intopval  48190  clintopval  48192  rngchomALTV  48256  funcringcsetcALTV2lem5  48282  ringchomALTV  48290  funcringcsetclem5ALTV  48305  srhmsubcALTVlem2  48312  srhmsubcALTV  48313  fldhmsubcALTV  48321  zlmodzxzscm  48345  zlmodzxzadd  48346  rmsupp0  48356  domnmsuppn0  48357  rmsuppss  48358  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  ply1mulgsum  48379  dmatALTval  48389  lincop  48397  lincval  48398  linc1  48414  lincresunit3lem1  48468  fdivmpt  48529  fdivmptfv  48534  refdivmptfv  48535  digval  48587  2arymptfv  48639  2arymaptfo  48643  itcovalpclem1  48659  itcovalt2lem1  48664  ackvalsuc1mpt  48667  ackval1  48670  ackval2  48671  ackval3  48672  ackval42  48685  line2xlem  48742  upfval2  49166  swapfval  49251  tposcurf1  49288  tposcurf2val  49290  fucofvalg  49307  fuco112x  49321  fuco23  49330  fucoid  49337  fucocolem4  49345  prcofvalg  49365  prcof1  49377  opf2fval  49394  lanval  49608  ranval  49609