Theorem ovexd 7384

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 7382	. 2 ⊢ (𝐴𝐹𝐵) ∈ V
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436  (class class class)co 7349

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 5245

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 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  caofidlcan  7651  caofass  7653  caofdi  7655  caofdir  7656  caonncan  7657  suppofssd  8136  mapsnend  8961  snmapen  8963  pw2eng  9000  mapen  9058  mapxpen  9060  mapunen  9063  mapdom2  9065  cantnfcl  9563  cantnfle  9567  cantnflt  9568  cantnflt2  9569  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1d  9584  cantnflem1  9585  cnfcomlem  9595  cnfcom  9596  cnfcom2lem  9597  cnfcom3lem  9599  fzen  13444  seqf1o  13950  wrdexg  14431  wrdnval  14452  pfxval  14580  pfxswrd  14612  splval  14657  cshwsexaOLD  14731  ofccat  14876  climshftlem  15481  climshft  15483  climshft2  15489  caucvgr  15583  fsumrev  15686  hashdvds  16686  setsabs  17090  ressress  17158  firest  17336  prdsvscafval  17384  qusval  17446  xpsbas  17476  xpsadd  17478  xpsmul  17479  xpssca  17480  xpsvsca  17481  xpsless  17482  xpsle  17483  homfval  17598  comfval  17606  cicfval  17704  rescabs  17740  rescabs2  17741  resscat  17759  funcres2c  17810  ressffth  17847  fucbas  17870  fuccoval  17873  setchom  17987  catchom  18010  catcco  18012  estrchom  18033  funcestrcsetclem5  18050  funcsetcestrclem5  18065  evlf2val  18125  curf11  18132  curf12  18133  curf2val  18136  uncfval  18140  diagval  18146  hof2  18163  yonval  18167  resspos  18335  gsumval2a  18559  gsumval2  18560  mndpsuppss  18639  gsumwspan  18720  efmnd  18744  ghmqusnsglem1  19159  ghmqusnsglem2  19160  ghmqusnsg  19161  ghmquskerlem1  19162  ghmquskerco  19163  ghmquskerlem2  19164  ghmquskerlem3  19165  ghmqusker  19166  orbstafun  19190  orbstaval  19191  symgval  19250  psgnvalii  19388  lsmhash  19584  frgpupval  19653  qusabl  19744  gsumval3  19786  gsumreidx  19796  gsumzaddlem  19800  gsummptshft  19815  telgsumfzslem  19867  telgsumfz  19869  telgsumfz0  19871  dpjval  19937  prdsrngd  20061  srgbinomlem3  20113  srgbinomlem4  20114  mulgass3  20238  rngcval  20503  rnghmsscmap2  20514  rnghmsscmap  20515  funcrngcsetc  20525  ringcval  20532  rhmsscmap2  20543  rhmsscmap  20544  funcringcsetc  20559  srhmsubclem3  20564  srhmsubc  20565  fldhmsubc  20670  lcomfsupp  20805  rmodislmodlem  20832  rmodislmod  20833  sraval  21079  srasca  21084  crngridl  21187  quscrng  21190  rhmqusnsg  21192  pzriprnglem11  21398  znval  21442  znzrhfo  21454  znunithash  21471  cygznlem2  21475  frobrhm  21482  pjfval  21613  pjpm  21615  frlmgsum  21679  frlmipval  21686  frlmphllem  21687  frlmphl  21688  frlmsslsp  21703  frlmup1  21705  gsumbagdiaglem  21837  psrass1lem  21839  rhmpsrlem1  21847  psrass1  21871  psrdi  21872  psrdir  21873  psrass23l  21874  psrascl  21886  mplval  21896  mplsubglem  21906  mplsubrglem  21911  mplmonmul  21941  mplcoe1  21942  opsrval  21951  psrbagev1  21982  psrbagev2  21983  evlslem6  21986  evlslem1  21987  evlsval  21991  mpfconst  22006  mpff  22009  mpfaddcl  22010  mpfmulcl  22011  mpfind  22012  mhpmulcl  22034  mhpaddcl  22036  psdcoef  22045  psdmplcl  22047  psdadd  22048  ply1lss  22079  gsumply1subr  22116  coe1add  22148  coe1tm  22157  coe1tmmul  22161  cply1mul  22181  ply1coe  22183  evl1expd  22230  pf1mpf  22237  pf1ind  22240  mhmcompl  22265  mhmcoaddmpl  22266  rhmmpl  22268  rhmply1vsca  22273  mamufv  22279  mamuass  22287  mamuvs1  22290  mamuvs2  22291  matgsum  22322  dmatmul  22382  scmatval  22389  scmatrhmval  22412  mvmulfv  22429  mavmulfv  22431  mavmulass  22434  marrepeval  22448  marepveval  22453  submaeval  22467  mdetrsca  22488  mdetunilem9  22505  mdetuni0  22506  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  smadiadetlem3  22553  cramerlem1  22572  mat2pmatmul  22616  m2cpminvid  22638  decpmatfsupp  22654  decpmatmullem  22656  decpmatmul  22657  decpmatmulsumfsupp  22658  pmatcollpw1lem1  22659  pmatcollpw3fi1lem1  22671  pmatcollpwscmatlem2  22675  pm2mpfval  22681  pm2mpf  22683  mply1topmatcllem  22688  mp2pm2mplem3  22693  mp2pm2mplem4  22694  pm2mpmhmlem1  22703  pm2mpmhmlem2  22704  pm2mp  22710  chfacfscmulfsupp  22744  chfacfscmulgsum  22745  chfacfpmmulfsupp  22748  chfacfpmmulgsum  22749  cpmidpmatlem3  22757  cpmadugsumlemB  22759  cpmadugsumlemC  22760  cpmadugsumlemF  22761  cayhamlem4  22773  xpstopnlem2  23696  fcfval  23918  tsmsxplem1  24038  tsmsxplem2  24039  tusval  24151  xpsdsfn  24263  xpsxmet  24266  xpsdsval  24267  xpsmet  24268  tmsval  24367  met1stc  24407  metuval  24435  cnmpopc  24820  pi1val  24935  pi1addf  24945  pi1addval  24946  pi1grplem  24947  rrxnm  25289  rrxcph  25290  rrxmval  25303  mbfmulc2  25562  mbfmul  25625  itg2mulclem  25645  ibladd  25720  itgadd  25724  itgabs  25734  bddmulibl  25738  dvmulf  25844  dvcmulf  25846  dvmptmul  25863  cmvth  25893  dvlip  25896  ftc1lem4  25944  mdegmullem  25981  coe1mul3  26002  r1pval  26061  plyco  26144  dgrcolem1  26177  elqaalem3  26227  taylpfval  26270  taylthlem2  26280  taylthlem2OLD  26281  pserdvlem2  26336  advlogexp  26562  logtayl  26567  logccv  26570  dvcxp1  26647  dvcncxp1  26650  logbmpt  26696  logbfval  26698  relogbf  26699  dvatan  26843  cxp2lim  26885  cxploglim2  26887  lgamgulmlem2  26938  lgamgulm2  26944  lgamcvglem  26948  lgamf  26950  basellem7  26995  basellem8  26996  basellem9  26997  fsumdvdscom  27093  logexprlim  27134  dchrfi  27164  gausslemma2dlem2  27276  gausslemma2dlem3  27277  2lgslem1b  27301  chtppilimlem2  27383  chebbnd2  27386  chto1lb  27387  chpchtlim  27388  chpo1ub  27389  vmadivsum  27391  dchrisum0lem3  27428  mudivsum  27439  logdivsum  27442  log2sumbnd  27453  selberglem1  27454  selberg2lem  27459  selberg2  27460  selbergr  27477  negsval  27938  wlkp1  29629  cyclnumvtx  29749  wwlksnextsurj  29849  wwlksnextbij  29851  clwlkclwwlklem2a1  29940  clwlkclwwlkf1  29958  eupth2eucrct  30165  frgrncvvdeq  30257  numclwlk2lem2fv  30326  numclwwlk2lem3  30328  ofoprabco  32615  fsuppcurry1  32676  fsuppcurry2  32677  offinsupp1  32678  ressprs  32917  mntoval  32933  mgcoval  32937  mndlactf1  32989  mndlactfo  32990  mndractf1  32991  mndractfo  32992  mndlactf1o  32993  mndractf1o  32994  lmodvslmhm  33012  gsumwrd2dccat  33029  cycpmco2f1  33075  cycpmco2rn  33076  cycpmco2lem2  33078  cycpmco2lem3  33079  cycpmco2lem4  33080  cycpmco2lem5  33081  cycpmco2lem6  33082  cycpmco2  33084  conjga  33121  cntrval2  33122  fxpsubm  33123  fxpsubg  33124  fxpsubrg  33125  fxpsdrg  33126  archirngz  33140  archiabllem2a  33145  elrgspnlem1  33191  elrgspnlem2  33192  elrgspnsubrunlem2  33197  rlocval  33208  fracval  33252  quslmod  33304  quslmhm  33305  quslvec  33306  qustriv  33310  qustrivr  33311  unitprodclb  33335  nsgmgc  33358  nsgqusf1olem1  33359  nsgqusf1olem2  33360  nsgqusf1olem3  33361  lmhmqusker  33363  rhmquskerlem  33371  elrspunidl  33374  qsidomlem1  33398  qsidomlem2  33399  opprqusbas  33434  opprqusplusg  33435  opprqusmulr  33437  opprqus1r  33438  qsdrngilem  33440  qsdrngi  33441  rprmdvdsprod  33480  1arithidomlem1  33481  1arithidomlem2  33482  1arithidom  33483  1arithufdlem3  33492  dfufd2lem  33495  zringfrac  33500  evl1deg1  33520  evl1deg2  33521  evl1deg3  33522  ply1gsumz  33540  r1plmhm  33551  mplvrpmrhm  33558  splyval  33561  resssra  33569  ply1degltdimlem  33605  ply1degltdim  33606  qusdimsum  33611  fedgmullem1  33612  fedgmullem2  33613  fedgmul  33614  lactlmhm  33617  fldgenfldext  33651  evls1fldgencl  33653  fldextrspunlsplem  33656  fldextrspundgdvdslem  33663  fldextrspundgdvds  33664  extdgfialglem1  33675  extdgfialglem2  33676  extdgfialg  33677  algextdeglem4  33703  algextdeglem6  33705  algextdeglem7  33706  submateq  33792  lmatcl  33799  mdetpmtr1  33806  madjusmdetlem1  33810  madjusmdetlem3  33812  qqhvval  33966  esumfzf  34052  esumpfinvallem  34057  esumpmono  34062  esummulc1  34064  esumcvg  34069  esumgect  34073  ofcval  34082  omssubadd  34284  sitgfval  34325  sitmcl  34335  sseqfv2  34378  cndprobval  34417  ballotlemfval  34474  ballotlemsv  34494  ballotlemsf1o  34498  ofcccat  34527  signsplypnf  34534  signsply0  34535  signstfval  34548  signshf  34572  reprpmtf1o  34610  reprdifc  34611  logdivsqrle  34634  hgt750lemg  34638  hgt750lema  34641  lpadval  34660  cvmliftlem8  35285  cvmliftphtlem  35310  fmla1  35380  gonarlem  35387  sategoelfvb  35412  mrsubval  35502  ellcsrspsn  35634  r1peuqusdeg1  35636  fwddifval  36156  knoppcnlem1  36487  knoppcnlem6  36492  unbdqndv2lem2  36504  poimirlem1  37621  poimirlem2  37622  poimirlem3  37623  poimirlem5  37625  poimirlem6  37626  poimirlem7  37627  poimirlem10  37630  poimirlem11  37631  poimirlem12  37632  poimirlem16  37636  poimirlem19  37639  poimirlem22  37642  poimirlem23  37643  broucube  37654  dvtan  37670  itg2addnc  37674  ibladdnc  37677  itgaddnc  37680  itgmulc2nclem2  37687  itgmulc2nc  37688  itgabsnc  37689  ftc1cnnclem  37691  ftc1anclem3  37695  ftc1anclem6  37698  ftc1anclem7  37699  ftc1anclem8  37700  dvasin  37704  dvacos  37705  dvreasin  37706  dvreacos  37707  areacirclem1  37708  areacirc  37713  fsumshftd  38951  hlrelat5N  39400  rhmzrhval  41964  aks6d1c1  42109  hashscontpow  42115  aks6d1c4  42117  aks6d1c2lem3  42119  aks6d1c2lem4  42120  aks6d1c2  42123  aks6d1c5lem0  42128  aks6d1c5lem3  42130  aks6d1c5lem2  42131  aks6d1c5  42132  sticksstones3  42141  sticksstones8  42146  sticksstones10  42148  sticksstones12a  42150  sticksstones12  42151  aks6d1c6lem1  42163  aks6d1c6lem2  42164  aks6d1c6lem3  42165  aks6d1c6lem4  42166  aks6d1c6isolem1  42167  aks6d1c6isolem2  42168  aks6d1c6isolem3  42169  aks6d1c6lem5  42170  aks6d1c7lem2  42174  unitscyglem1  42188  readvrec2  42354  readvrec  42355  readvcot  42357  frlmfzolen  42496  frlmfzoccat  42498  frlmvscadiccat  42499  evlscl  42551  evlsval3  42552  evlsvval  42553  evlsvvval  42556  evlsbagval  42559  evlsexpval  42560  evlsaddval  42561  evlsmulval  42562  evlsevl  42564  evlcl  42565  evladdval  42568  evlmulval  42569  selvcl  42576  evlselv  42580  fsuppind  42583  mhpind  42587  mhphflem  42589  prjspner  42612  prjspnvs  42613  prjspnfv01  42617  prjspner01  42618  prjspner1  42619  0prjspnrel  42620  prjcrv0  42626  mzpclall  42720  mzpsubst  42741  eldioph2  42755  rabdiophlem2  42795  irrapxlem1  42815  mzpcong  42965  mendlmod  43182  naddcnff  43355  relexpmulnn  43702  iunrelexpuztr  43712  mnringvald  44206  mnringmulrvald  44220  radcnvrat  44307  hashnzfzclim  44315  lhe4.4ex1a  44322  expgrowthi  44326  expgrowth  44328  bccval  44331  binomcxplemrat  44343  binomcxplemfrat  44344  binomcxplemradcnv  44345  binomcxplemdvbinom  44346  binomcxplemdvsum  44348  binomcxplemnotnn0  44349  unirnmap  45206  unirnmapsn  45212  ssmapsn  45214  iocopn  45521  icoopn  45526  divcnvg  45628  sumnnodd  45631  climsubmpt  45661  dvsinax  45914  fperdvper  45920  dvdivf  45923  dvnprodlem1  45947  itgsincmulx  45975  stoweidlem59  46060  etransclem4  46239  etransclem13  46248  etransclem25  46260  etransclem48  46283  rrxtopnfi  46288  sge0tsms  46381  elhoi  46543  ovnval2  46546  ovnval2b  46553  ovncvrrp  46565  ovn0lem  46566  ovncl  46568  ovnome  46574  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvle  46601  ovnlecvr2  46611  ovncvr2  46612  ovnsubadd2lem  46646  ovnovollem1  46657  vonvolmbl  46662  iunhoiioolem  46676  vonioolem1  46681  vonioolem2  46682  vonicclem2  46685  smfresal  46789  smfres  46791  smfmullem4  46795  smfco  46803  adddmmbl  46834  muldmmbl  46836  sinnpoly  46895  fmtno  47533  isubgruhgr  47872  grtriprop  47945  grtriclwlk3  47949  gpgvtx  48047  gpgiedg  48048  intopval  48206  clintopval  48208  rngchomALTV  48272  funcringcsetcALTV2lem5  48298  ringchomALTV  48306  funcringcsetclem5ALTV  48321  srhmsubcALTVlem2  48328  srhmsubcALTV  48329  fldhmsubcALTV  48337  zlmodzxzscm  48361  zlmodzxzadd  48362  rmsupp0  48372  domnmsuppn0  48373  rmsuppss  48374  ply1mulgsumlem3  48393  ply1mulgsumlem4  48394  ply1mulgsum  48395  dmatALTval  48405  lincop  48413  lincval  48414  linc1  48430  lincresunit3lem1  48484  fdivmpt  48545  fdivmptfv  48550  refdivmptfv  48551  digval  48603  2arymptfv  48655  2arymaptfo  48659  itcovalpclem1  48675  itcovalt2lem1  48680  ackvalsuc1mpt  48683  ackval1  48686  ackval2  48687  ackval3  48688  ackval42  48701  line2xlem  48758  upfval2  49182  swapfval  49267  tposcurf1  49304  tposcurf2val  49306  fucofvalg  49323  fuco112x  49337  fuco23  49346  fucoid  49353  fucocolem4  49361  prcofvalg  49381  prcof1  49393  opf2fval  49410  lanval  49624  ranval  49625