Theorem ovexd 7444

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  caofass  7707  caofdi  7709  caofdir  7710  caonncan  7711  suppofssd  8188  mapsnend  9036  snmapen  9038  pw2eng  9078  mapen  9141  mapxpen  9143  mapunen  9146  mapdom2  9148  cantnfcl  9662  cantnfle  9666  cantnflt  9667  cantnflt2  9668  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1d  9683  cantnflem1  9684  cnfcomlem  9694  cnfcom  9695  cnfcom2lem  9696  cnfcom3lem  9698  fzen  13518  seqf1o  14009  wrdexg  14474  wrdnval  14495  pfxval  14623  pfxswrd  14656  splval  14701  cshwsexaOLD  14775  ofccat  14916  climshftlem  15518  climshft  15520  climshft2  15526  caucvgr  15622  fsumrev  15725  hashdvds  16708  setsabs  17112  ressress  17193  firest  17378  prdsvscafval  17426  qusval  17488  xpsbas  17518  xpsadd  17520  xpsmul  17521  xpssca  17522  xpsvsca  17523  xpsless  17524  xpsle  17525  homfval  17636  comfval  17644  cicfval  17744  rescabs  17782  rescabsOLD  17783  rescabs2  17784  resscat  17802  funcres2c  17852  ressffth  17889  fucbas  17912  fuccoval  17916  setchom  18030  catchom  18053  catcco  18055  estrchom  18078  funcestrcsetclem5  18096  funcsetcestrclem5  18111  evlf2val  18172  curf11  18179  curf12  18180  curf2val  18183  uncfval  18187  diagval  18193  hof2  18210  yonval  18214  gsumval2a  18604  gsumval2  18605  gsumwspan  18727  efmnd  18751  orbstafun  19175  orbstaval  19176  symgval  19236  psgnvalii  19377  lsmhash  19573  frgpupval  19642  qusabl  19733  gsumval3  19775  gsumreidx  19785  gsumzaddlem  19789  gsummptshft  19804  telgsumfzslem  19856  telgsumfz  19858  telgsumfz0  19860  dpjval  19926  srgbinomlem3  20051  srgbinomlem4  20052  mulgass3  20167  lcomfsupp  20512  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  sraval  20789  srasca  20798  srascaOLD  20799  crngridl  20876  quscrng  20878  znval  21087  znzrhfo  21103  znunithash  21120  cygznlem2  21124  pjfval  21261  pjpm  21263  frlmgsum  21327  frlmipval  21334  frlmphllem  21335  frlmphl  21336  frlmsslsp  21351  frlmup1  21353  gsumbagdiaglemOLD  21491  psrass1lemOLD  21493  gsumbagdiaglem  21494  psrass1lem  21496  psrass1  21525  psrdi  21526  psrdir  21527  psrass23l  21528  mplval  21548  mplsubglem  21558  mplsubrglem  21563  mplmonmul  21591  mplcoe1  21592  opsrval  21601  psrbagev1  21638  psrbagev1OLD  21639  psrbagev2  21640  evlslem6  21644  evlslem1  21645  evlsval  21649  mpfconst  21664  mpff  21667  mpfaddcl  21668  mpfmulcl  21669  mpfind  21670  mhpmulcl  21692  mhpaddcl  21694  mhpvscacl  21697  ply1lss  21720  gsumply1subr  21756  coe1add  21786  coe1tm  21795  coe1tmmul  21799  cply1mul  21818  ply1coe  21820  evl1expd  21864  pf1mpf  21871  pf1ind  21874  mamufv  21889  mamuass  21902  mamuvs1  21905  mamuvs2  21906  matgsum  21939  dmatmul  21999  scmatval  22006  scmatrhmval  22029  mvmulfv  22046  mavmulfv  22048  mavmulass  22051  marrepeval  22065  marepveval  22070  submaeval  22084  mdetrsca  22105  mdetunilem9  22122  mdetuni0  22123  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  smadiadetlem3  22170  cramerlem1  22189  mat2pmatmul  22233  m2cpminvid  22255  decpmatfsupp  22271  decpmatmullem  22273  decpmatmul  22274  decpmatmulsumfsupp  22275  pmatcollpw1lem1  22276  pmatcollpw3fi1lem1  22288  pmatcollpwscmatlem2  22292  pm2mpfval  22298  pm2mpf  22300  mply1topmatcllem  22305  mp2pm2mplem3  22310  mp2pm2mplem4  22311  pm2mpmhmlem1  22320  pm2mpmhmlem2  22321  pm2mp  22327  chfacfscmulfsupp  22361  chfacfscmulgsum  22362  chfacfpmmulfsupp  22365  chfacfpmmulgsum  22366  cpmidpmatlem3  22374  cpmadugsumlemB  22376  cpmadugsumlemC  22377  cpmadugsumlemF  22378  cayhamlem4  22390  xpstopnlem2  23315  fcfval  23537  tsmsxplem1  23657  tsmsxplem2  23658  tusval  23770  xpsdsfn  23883  xpsxmet  23886  xpsdsval  23887  xpsmet  23888  tmsval  23989  met1stc  24030  metuval  24058  cnmpopc  24444  pi1val  24553  pi1addf  24563  pi1addval  24564  pi1grplem  24565  rrxnm  24908  rrxcph  24909  rrxmval  24922  mbfmulc2  25180  mbfmul  25244  itg2mulclem  25264  ibladd  25338  itgadd  25342  itgabs  25352  bddmulibl  25356  dvmulf  25460  dvcmulf  25462  dvmptmul  25478  dvlip  25510  ftc1lem4  25556  mdegmullem  25596  coe1mul3  25617  r1pval  25674  plyco  25755  dgrcolem1  25787  elqaalem3  25834  taylpfval  25877  taylthlem2  25886  pserdvlem2  25940  advlogexp  26163  logtayl  26168  logccv  26171  dvcxp1  26248  dvcncxp1  26251  logbmpt  26293  logbfval  26295  relogbf  26296  dvatan  26440  cxp2lim  26481  cxploglim2  26483  lgamgulmlem2  26534  lgamgulm2  26540  lgamcvglem  26544  lgamf  26546  basellem7  26591  basellem8  26592  basellem9  26593  fsumdvdscom  26689  logexprlim  26728  dchrfi  26758  gausslemma2dlem2  26870  gausslemma2dlem3  26871  2lgslem1b  26895  chtppilimlem2  26977  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  vmadivsum  26985  dchrisum0lem3  27022  mudivsum  27033  logdivsum  27036  log2sumbnd  27047  selberglem1  27048  selberg2lem  27053  selberg2  27054  selbergr  27071  negsval  27503  wlkp1  28969  wwlksnextsurj  29185  wwlksnextbij  29187  clwlkclwwlklem2a1  29276  clwlkclwwlkf1  29294  eupth2eucrct  29501  frgrncvvdeq  29593  numclwlk2lem2fv  29662  numclwwlk2lem3  29664  ofoprabco  31920  fsuppcurry1  31981  fsuppcurry2  31982  offinsupp1  31983  ressprs  32164  resspos  32167  mntoval  32183  mgcoval  32187  lmodvslmhm  32233  cycpmco2f1  32314  cycpmco2rn  32315  cycpmco2lem2  32317  cycpmco2lem3  32318  cycpmco2lem4  32319  cycpmco2lem5  32320  cycpmco2lem6  32321  cycpmco2  32323  archirngz  32366  archiabllem2a  32371  frobrhm  32413  quslmod  32500  quslmhm  32501  quslvec  32502  qustriv  32507  qustrivr  32508  nsgmgc  32554  nsgqusf1olem1  32555  nsgqusf1olem2  32556  nsgqusf1olem3  32557  ghmquskerlem1  32559  ghmquskerco  32560  ghmquskerlem2  32561  ghmquskerlem3  32562  ghmqusker  32563  lmhmqusker  32565  rhmquskerlem  32574  elrspunidl  32577  qsidomlem1  32602  qsidomlem2  32603  opprqusbas  32633  opprqusplusg  32634  opprqusmulr  32636  opprqus1r  32637  qsdrngilem  32639  qsdrngi  32640  ply1gsumz  32700  ply1degltdimlem  32738  ply1degltdim  32739  qusdimsum  32744  fedgmullem1  32745  fedgmullem2  32746  fedgmul  32747  algextdeglem1  32803  submateq  32820  lmatcl  32827  mdetpmtr1  32834  madjusmdetlem1  32838  madjusmdetlem3  32840  qqhvval  32994  esumfzf  33098  esumpfinvallem  33103  esumpmono  33108  esummulc1  33110  esumcvg  33115  esumgect  33119  ofcval  33128  omssubadd  33330  sitgfval  33371  sitmcl  33381  sseqfv2  33424  cndprobval  33463  ballotlemfval  33519  ballotlemsv  33539  ballotlemsf1o  33543  ofcccat  33585  signsplypnf  33592  signsply0  33593  signstfval  33606  signshf  33630  reprpmtf1o  33669  reprdifc  33670  logdivsqrle  33693  hgt750lemg  33697  hgt750lema  33700  lpadval  33719  cvmliftlem8  34314  cvmliftphtlem  34339  fmla1  34409  gonarlem  34416  sategoelfvb  34441  mrsubval  34531  fwddifval  35165  gg-cmvth  35212  knoppcnlem1  35417  knoppcnlem6  35422  unbdqndv2lem2  35434  poimirlem1  36537  poimirlem2  36538  poimirlem3  36539  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem16  36552  poimirlem19  36555  poimirlem22  36558  poimirlem23  36559  broucube  36570  dvtan  36586  itg2addnc  36590  ibladdnc  36593  itgaddnc  36596  itgmulc2nclem2  36603  itgmulc2nc  36604  itgabsnc  36605  ftc1cnnclem  36607  ftc1anclem3  36611  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anclem8  36616  dvasin  36620  dvacos  36621  dvreasin  36622  dvreacos  36623  areacirclem1  36624  areacirc  36629  fsumshftd  37870  hlrelat5N  38320  sticksstones3  41012  sticksstones8  41017  sticksstones10  41019  sticksstones12a  41021  sticksstones12  41022  frlmfzolen  41125  frlmfzoccat  41127  frlmvscadiccat  41128  rhmmpllem1  41169  rhmmpl  41173  evlscl  41178  evlsval3  41179  evlsvval  41180  evlsvvval  41183  evlsbagval  41186  evlsexpval  41187  evlsaddval  41188  evlsmulval  41189  evlsevl  41191  evlcl  41192  evladdval  41195  evlmulval  41196  selvcl  41203  evlselv  41207  fsuppind  41210  mhpind  41214  mhphflem  41216  prjspner  41409  prjspnvs  41410  prjspnfv01  41414  prjspner01  41415  prjspner1  41416  0prjspnrel  41417  prjcrv0  41423  mzpclall  41513  mzpsubst  41534  eldioph2  41548  rabdiophlem2  41588  irrapxlem1  41608  mzpcong  41759  mendlmod  41983  naddcnff  42160  relexpmulnn  42508  iunrelexpuztr  42518  mnringvald  43015  mnringmulrvald  43034  radcnvrat  43121  hashnzfzclim  43129  lhe4.4ex1a  43136  expgrowthi  43140  expgrowth  43142  bccval  43145  binomcxplemrat  43157  binomcxplemfrat  43158  binomcxplemradcnv  43159  binomcxplemdvbinom  43160  binomcxplemdvsum  43162  binomcxplemnotnn0  43163  unirnmap  43955  unirnmapsn  43961  ssmapsn  43963  iocopn  44281  icoopn  44286  divcnvg  44391  sumnnodd  44394  climsubmpt  44424  dvsinax  44677  fperdvper  44683  dvdivf  44686  dvnprodlem1  44710  itgsincmulx  44738  stoweidlem59  44823  etransclem4  45002  etransclem13  45011  etransclem25  45023  etransclem48  45046  rrxtopnfi  45051  sge0tsms  45144  elhoi  45306  ovnval2  45309  ovnval2b  45316  ovncvrrp  45328  ovn0lem  45329  ovncl  45331  ovnome  45337  hoidmvlelem2  45360  hoidmvlelem3  45361  hoidmvle  45364  ovnlecvr2  45374  ovncvr2  45375  ovnsubadd2lem  45409  ovnovollem1  45420  vonvolmbl  45425  iunhoiioolem  45439  vonioolem1  45444  vonioolem2  45445  vonicclem2  45448  smfresal  45552  smfres  45554  smfmullem4  45558  smfco  45566  adddmmbl  45597  muldmmbl  45599  fmtno  46245  intopval  46660  clintopval  46662  prdsrngd  46725  pzriprnglem11  46863  rngcval  46908  rnghmsscmap2  46919  rnghmsscmap  46920  rngchomALTV  46931  funcrngcsetc  46944  ringcval  46954  rhmsscmap2  46965  rhmsscmap  46966  funcringcsetc  46981  funcringcsetcALTV2lem5  46986  ringchomALTV  46994  funcringcsetclem5ALTV  47009  srhmsubclem3  47021  srhmsubc  47022  fldhmsubc  47030  srhmsubcALTVlem2  47039  srhmsubcALTV  47040  fldhmsubcALTV  47048  zlmodzxzscm  47081  zlmodzxzadd  47082  rmsupp0  47092  domnmsuppn0  47093  rmsuppss  47094  mndpsuppss  47095  ply1mulgsumlem3  47117  ply1mulgsumlem4  47118  ply1mulgsum  47119  dmatALTval  47129  lincop  47137  lincval  47138  linc1  47154  lincresunit3lem1  47208  fdivmpt  47274  fdivmptfv  47279  refdivmptfv  47280  digval  47332  2arymptfv  47384  2arymaptfo  47388  itcovalpclem1  47404  itcovalt2lem1  47409  ackvalsuc1mpt  47412  ackval1  47415  ackval2  47416  ackval3  47417  ackval42  47430  line2xlem  47487