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  27500  wlkp1  28938  wwlksnextsurj  29154  wwlksnextbij  29156  clwlkclwwlklem2a1  29245  clwlkclwwlkf1  29263  eupth2eucrct  29470  frgrncvvdeq  29562  numclwlk2lem2fv  29631  numclwwlk2lem3  29633  ofoprabco  31889  fsuppcurry1  31950  fsuppcurry2  31951  offinsupp1  31952  ressprs  32133  resspos  32136  mntoval  32152  mgcoval  32156  lmodvslmhm  32202  cycpmco2f1  32283  cycpmco2rn  32284  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  archirngz  32335  archiabllem2a  32340  frobrhm  32382  quslmod  32469  quslmhm  32470  quslvec  32471  qustriv  32476  qustrivr  32477  nsgmgc  32523  nsgqusf1olem1  32524  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem1  32528  ghmquskerco  32529  ghmquskerlem2  32530  ghmquskerlem3  32531  ghmqusker  32532  lmhmqusker  32534  rhmquskerlem  32543  elrspunidl  32546  qsidomlem1  32571  qsidomlem2  32572  opprqusbas  32602  opprqusplusg  32603  opprqusmulr  32605  opprqus1r  32606  qsdrngilem  32608  qsdrngi  32609  ply1gsumz  32669  ply1degltdimlem  32707  ply1degltdim  32708  qusdimsum  32713  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  algextdeglem1  32772  submateq  32789  lmatcl  32796  mdetpmtr1  32803  madjusmdetlem1  32807  madjusmdetlem3  32809  qqhvval  32963  esumfzf  33067  esumpfinvallem  33072  esumpmono  33077  esummulc1  33079  esumcvg  33084  esumgect  33088  ofcval  33097  omssubadd  33299  sitgfval  33340  sitmcl  33350  sseqfv2  33393  cndprobval  33432  ballotlemfval  33488  ballotlemsv  33508  ballotlemsf1o  33512  ofcccat  33554  signsplypnf  33561  signsply0  33562  signstfval  33575  signshf  33599  reprpmtf1o  33638  reprdifc  33639  logdivsqrle  33662  hgt750lemg  33666  hgt750lema  33669  lpadval  33688  cvmliftlem8  34283  cvmliftphtlem  34308  fmla1  34378  gonarlem  34385  sategoelfvb  34410  mrsubval  34500  fwddifval  35134  gg-cmvth  35181  knoppcnlem1  35369  knoppcnlem6  35374  unbdqndv2lem2  35386  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem19  36507  poimirlem22  36510  poimirlem23  36511  broucube  36522  dvtan  36538  itg2addnc  36542  ibladdnc  36545  itgaddnc  36548  itgmulc2nclem2  36555  itgmulc2nc  36556  itgabsnc  36557  ftc1cnnclem  36559  ftc1anclem3  36563  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  dvasin  36572  dvacos  36573  dvreasin  36574  dvreacos  36575  areacirclem1  36576  areacirc  36581  fsumshftd  37822  hlrelat5N  38272  sticksstones3  40964  sticksstones8  40969  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  frlmfzolen  41077  frlmfzoccat  41079  frlmvscadiccat  41080  rhmmpllem1  41121  rhmmpl  41125  evlscl  41130  evlsval3  41131  evlsvval  41132  evlsvvval  41135  evlsbagval  41138  evlsexpval  41139  evlsaddval  41140  evlsmulval  41141  evlsevl  41143  evlcl  41144  evladdval  41147  evlmulval  41148  selvcl  41155  evlselv  41159  fsuppind  41162  mhpind  41166  mhphflem  41168  prjspner  41361  prjspnvs  41362  prjspnfv01  41366  prjspner01  41367  prjspner1  41368  0prjspnrel  41369  prjcrv0  41375  mzpclall  41465  mzpsubst  41486  eldioph2  41500  rabdiophlem2  41540  irrapxlem1  41560  mzpcong  41711  mendlmod  41935  naddcnff  42112  relexpmulnn  42460  iunrelexpuztr  42470  mnringvald  42967  mnringmulrvald  42986  radcnvrat  43073  hashnzfzclim  43081  lhe4.4ex1a  43088  expgrowthi  43092  expgrowth  43094  bccval  43097  binomcxplemrat  43109  binomcxplemfrat  43110  binomcxplemradcnv  43111  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  unirnmap  43907  unirnmapsn  43913  ssmapsn  43915  iocopn  44233  icoopn  44238  divcnvg  44343  sumnnodd  44346  climsubmpt  44376  dvsinax  44629  fperdvper  44635  dvdivf  44638  dvnprodlem1  44662  itgsincmulx  44690  stoweidlem59  44775  etransclem4  44954  etransclem13  44963  etransclem25  44975  etransclem48  44998  rrxtopnfi  45003  sge0tsms  45096  elhoi  45258  ovnval2  45261  ovnval2b  45268  ovncvrrp  45280  ovn0lem  45281  ovncl  45283  ovnome  45289  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvle  45316  ovnlecvr2  45326  ovncvr2  45327  ovnsubadd2lem  45361  ovnovollem1  45372  vonvolmbl  45377  iunhoiioolem  45391  vonioolem1  45396  vonioolem2  45397  vonicclem2  45400  smfresal  45504  smfres  45506  smfmullem4  45510  smfco  45518  adddmmbl  45549  muldmmbl  45551  fmtno  46197  intopval  46612  clintopval  46614  prdsrngd  46677  pzriprnglem11  46815  rngcval  46860  rnghmsscmap2  46871  rnghmsscmap  46872  rngchomALTV  46883  funcrngcsetc  46896  ringcval  46906  rhmsscmap2  46917  rhmsscmap  46918  funcringcsetc  46933  funcringcsetcALTV2lem5  46938  ringchomALTV  46946  funcringcsetclem5ALTV  46961  srhmsubclem3  46973  srhmsubc  46974  fldhmsubc  46982  srhmsubcALTVlem2  46991  srhmsubcALTV  46992  fldhmsubcALTV  47000  zlmodzxzscm  47033  zlmodzxzadd  47034  rmsupp0  47044  domnmsuppn0  47045  rmsuppss  47046  mndpsuppss  47047  ply1mulgsumlem3  47069  ply1mulgsumlem4  47070  ply1mulgsum  47071  dmatALTval  47081  lincop  47089  lincval  47090  linc1  47106  lincresunit3lem1  47160  fdivmpt  47226  fdivmptfv  47231  refdivmptfv  47232  digval  47284  2arymptfv  47336  2arymaptfo  47340  itcovalpclem1  47356  itcovalt2lem1  47361  ackvalsuc1mpt  47364  ackval1  47367  ackval2  47368  ackval3  47369  ackval42  47382  line2xlem  47439