Theorem ovexd 7446

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  caofidlcan  7713  caofass  7715  caofdi  7717  caofdir  7718  caonncan  7719  suppofssd  8199  mapsnend  9033  snmapen  9035  pw2eng  9071  mapen  9129  mapxpen  9131  mapunen  9134  mapdom2  9136  cantnfcl  9636  cantnfle  9640  cantnflt  9641  cantnflt2  9642  cantnfp1lem2  9648  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1d  9657  cantnflem1  9658  cnfcomlem  9668  cnfcom  9669  cnfcom2lem  9670  cnfcom3lem  9672  fzen  13569  seqf1o  14079  wrdexg  14561  wrdnval  14582  pfxval  14711  pfxswrd  14743  splval  14788  ofccat  15006  climshftlem  15625  climshft  15627  climshft2  15633  caucvgr  15727  fsumrev  15830  hashdvds  16834  setsabs  17239  ressress  17307  firest  17485  prdsvscafval  17533  qusval  17596  xpsbas  17626  xpsadd  17628  xpsmul  17629  xpssca  17630  xpsvsca  17631  xpsless  17632  xpsle  17633  homfval  17748  comfval  17756  cicfval  17854  rescabs  17890  rescabs2  17891  resscat  17909  funcres2c  17960  ressffth  17997  fucbas  18020  fuccoval  18023  setchom  18137  catchom  18160  catcco  18162  estrchom  18183  funcestrcsetclem5  18200  funcsetcestrclem5  18215  evlf2val  18275  curf11  18282  curf12  18283  curf2val  18286  uncfval  18290  diagval  18296  hof2  18313  yonval  18317  resspos  18485  gsumval2a  18743  gsumval2  18744  mndpsuppss  18823  gsumwspan  18905  efmnd  18929  qustriv  19252  qustrivr  19253  ghmqusnsglem1  19350  ghmqusnsglem2  19351  ghmqusnsg  19352  ghmquskerlem1  19353  ghmquskerco  19354  ghmquskerlem2  19355  ghmquskerlem3  19356  ghmqusker  19357  orbstafun  19381  orbstaval  19382  symgval  19441  psgnvalii  19579  lsmhash  19775  frgpupval  19844  qusabl  19935  gsumval3  19977  gsumreidx  19987  gsumzaddlem  19991  gsummptshft  20006  telgsumfzslem  20058  telgsumfz  20060  telgsumfz0  20062  dpjval  20128  prdsrngd  20254  srgbinomlem3  20310  srgbinomlem4  20311  mulgass3  20435  rngcval  20703  rnghmsscmap2  20714  rnghmsscmap  20715  funcrngcsetc  20725  ringcval  20732  rhmsscmap2  20743  rhmsscmap  20744  funcringcsetc  20759  srhmsubclem3  20764  srhmsubc  20765  fldhmsubc  20866  lcomfsupp  21001  rmodislmodlem  21028  rmodislmod  21029  sraval  21274  srasca  21279  crngridl  21390  quscrng  21394  rhmqusnsg  21396  qsidomlem1  21449  qsidomlem2  21450  pzriprnglem11  21610  znval  21654  znzrhfo  21666  znunithash  21683  cygznlem2  21687  frobrhm  21694  pjfval  21825  pjpm  21827  frlmgsum  21891  frlmipval  21898  frlmphllem  21899  frlmphl  21900  frlmsslsp  21915  frlmup1  21917  gsumbagdiaglem  22050  psrass1lem  22052  rhmpsrlem1  22059  psrass1  22082  psrdi  22083  psrdir  22084  psrass23l  22085  psrascl  22097  mplval  22107  mplsubglem  22117  mplsubrglem  22122  mplmonmul  22156  mplcoe1  22157  opsrval  22166  psrbagev1  22197  psrbagev2  22198  evlslem6  22201  evlslem1  22202  evlsval  22206  evlsval3  22209  evlsvval  22210  evlsvvval  22213  evlcl  22222  evladdval  22223  evlmulval  22224  mpfconst  22229  mpff  22232  mpfaddcl  22233  mpfmulcl  22234  mpfind  22235  mhmcompl  22241  mhmcoaddmpl  22243  evlscl  22245  evlsexpval  22248  evlsaddval  22249  evlsmulval  22250  evlsevl  22252  selvcl  22260  mhpmulcl  22281  mhpaddcl  22283  psdcoef  22292  psdmplcl  22294  psdadd  22295  ply1lss  22325  gsumply1subr  22362  coe1add  22394  coe1tm  22403  coe1tmmul  22407  cply1mul  22425  ply1coe  22427  evl1expd  22474  pf1mpf  22481  pf1ind  22484  rhmmpl  22509  rhmply1vsca  22514  mamufv  22520  mamuass  22528  mamuvs1  22531  mamuvs2  22532  matgsum  22563  dmatmul  22623  scmatval  22630  scmatrhmval  22653  mvmulfv  22670  mavmulfv  22672  mavmulass  22675  marrepeval  22689  marepveval  22694  submaeval  22708  mdetrsca  22729  mdetunilem9  22746  mdetuni0  22747  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  smadiadetlem3  22794  cramerlem1  22813  mat2pmatmul  22857  m2cpminvid  22879  decpmatfsupp  22895  decpmatmullem  22897  decpmatmul  22898  decpmatmulsumfsupp  22899  pmatcollpw1lem1  22900  pmatcollpw3fi1lem1  22912  pmatcollpwscmatlem2  22916  pm2mpfval  22922  pm2mpf  22924  mply1topmatcllem  22929  mp2pm2mplem3  22934  mp2pm2mplem4  22935  pm2mpmhmlem1  22944  pm2mpmhmlem2  22945  pm2mp  22951  chfacfscmulfsupp  22985  chfacfscmulgsum  22986  chfacfpmmulfsupp  22989  chfacfpmmulgsum  22990  cpmidpmatlem3  22998  cpmadugsumlemB  23000  cpmadugsumlemC  23001  cpmadugsumlemF  23002  cayhamlem4  23014  xpstopnlem2  23937  fcfval  24159  tsmsxplem1  24279  tsmsxplem2  24280  tusval  24391  xpsdsfn  24503  xpsxmet  24506  xpsdsval  24507  xpsmet  24508  tmsval  24607  met1stc  24647  metuval  24675  cnmpopc  25056  pi1val  25165  pi1addf  25175  pi1addval  25176  pi1grplem  25177  rrxnm  25519  rrxcph  25520  rrxmval  25533  mbfmulc2  25791  mbfmul  25854  itg2mulclem  25874  ibladd  25949  itgadd  25953  itgabs  25963  bddmulibl  25967  dvmulf  26071  dvcmulf  26073  dvmptmul  26089  cmvth  26119  dvlip  26121  ftc1lem4  26167  mdegmullem  26204  coe1mul3  26225  r1pval  26284  plyco  26367  dgrcolem1  26399  elqaalem3  26451  taylpfval  26494  taylthlem2  26503  pserdvlem2  26557  advlogexp  26786  logtayl  26791  logccv  26794  dvcxp1  26871  dvcncxp1  26874  logbmpt  26919  logbfval  26921  relogbf  26922  dvatan  27066  cxp2lim  27107  cxploglim2  27109  lgamgulmlem2  27160  lgamgulm2  27166  lgamcvglem  27170  lgamf  27172  basellem7  27217  basellem8  27218  basellem9  27219  fsumdvdscom  27315  logexprlim  27355  dchrfi  27385  gausslemma2dlem2  27497  gausslemma2dlem3  27498  2lgslem1b  27522  chtppilimlem2  27604  chebbnd2  27607  chto1lb  27608  chpchtlim  27609  chpo1ub  27610  vmadivsum  27612  dchrisum0lem3  27649  mudivsum  27660  logdivsum  27663  log2sumbnd  27674  selberglem1  27675  selberg2lem  27680  selberg2  27681  selbergr  27698  negsval  28184  wlkp1  29970  cyclnumvtx  30090  wwlksnextsurj  30190  wwlksnextbij  30192  clwlkclwwlklem2a1  30284  clwlkclwwlkf1  30302  eupth2eucrct  30509  frgrncvvdeq  30601  numclwlk2lem2fv  30670  numclwwlk2lem3  30672  ofoprabco  32950  fsuppcurry1  33010  fsuppcurry2  33011  offinsupp1  33012  ressprs  33227  mntoval  33243  mgcoval  33247  mndlactf1  33287  mndlactfo  33288  mndractf1  33289  mndractfo  33290  mndlactf1o  33291  mndractf1o  33292  lmodvslmhm  33311  gsummulsubdishift2  33330  gsumwrd2dccat  33339  cycpmco2f1  33385  cycpmco2rn  33386  cycpmco2lem2  33388  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2  33394  conjga  33431  cntrval2  33432  fxpsubm  33433  fxpsubg  33434  fxpsubrg  33435  fxpsdrg  33436  archirngz  33450  archiabllem2a  33455  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnsubrunlem2  33509  rlocval  33520  fracval  33568  quslmod  33621  quslmhm  33622  quslvec  33623  unitprodclb  33646  nsgmgc  33665  nsgqusf1olem1  33666  nsgqusf1olem2  33667  nsgqusf1olem3  33668  lmhmqusker  33670  rhmquskerlem  33677  elrspunidl  33680  opprqusbas  33715  opprqusplusg  33716  opprqusmulr  33718  opprqus1r  33719  qsdrngilem  33721  qsdrngi  33722  rprmdvdsprod  33769  1arithidomlem1  33770  1arithidomlem2  33771  1arithidom  33772  1arithufdlem3  33781  dfufd2lem  33784  zringfrac  33789  evl1deg1  33811  evl1deg2  33812  evl1deg3  33813  ply1gsumz  33834  r1plmhm  33844  0mplrim  33849  selvply1rhmlema  33853  selvply1rhmlemb  33854  selvply1rhmlem1  33855  selvply1rhmlem3  33857  selvply1rhmlem4  33858  selvply1rhmlem5  33859  mplvrpmrhm  33882  psrgsum  33883  psrmonmul  33885  psrmonprod  33887  mplgsum  33888  splyval  33894  esplyfval1  33908  esplyfvaln  33909  vietadeg1  33913  resssra  33922  ply1degltdimlem  33957  ply1degltdim  33958  qusdimsum  33963  fedgmullem1  33964  fedgmullem2  33965  fedgmul  33966  lactlmhm  33969  fldgenfldext  34003  evls1fldgencl  34005  fldextrspunlsplem  34008  fldextrspundgdvdslem  34015  fldextrspundgdvds  34016  extdgfialglem1  34027  extdgfialglem2  34028  extdgfialg  34029  algextdeglem4  34055  algextdeglem6  34057  algextdeglem7  34058  submateq  34144  lmatcl  34151  mdetpmtr1  34158  madjusmdetlem1  34162  madjusmdetlem3  34164  qqhvval  34318  esumfzf  34404  esumpfinvallem  34409  esumpmono  34414  esummulc1  34416  esumcvg  34421  esumgect  34425  ofcval  34434  omssubadd  34635  sitgfval  34676  sitmcl  34686  sseqfv2  34729  cndprobval  34768  ballotlemfval  34825  ballotlemsv  34845  ballotlemsf1o  34849  ofcccat  34878  signsplypnf  34882  signsply0  34883  signstfval  34896  signshf  34920  reprpmtf1o  34958  reprdifc  34959  logdivsqrle  34982  hgt750lemg  34986  hgt750lema  34989  lpadval  35011  cvmliftlem8  35717  cvmliftphtlem  35742  fmla1  35812  gonarlem  35819  sategoelfvb  35844  mrsubval  35934  ellcsrspsn  36066  r1peuqusdeg1  36068  fwddifval  36587  knoppcnlem1  37005  knoppcnlem6  37010  unbdqndv2lem2  37022  poimirlem1  38195  poimirlem2  38196  poimirlem3  38197  poimirlem5  38199  poimirlem6  38200  poimirlem7  38201  poimirlem10  38204  poimirlem11  38205  poimirlem12  38206  poimirlem16  38210  poimirlem19  38213  poimirlem22  38216  poimirlem23  38217  broucube  38228  dvtan  38244  itg2addnc  38248  ibladdnc  38251  itgaddnc  38254  itgmulc2nclem2  38261  itgmulc2nc  38262  itgabsnc  38263  ftc1cnnclem  38265  ftc1anclem3  38269  ftc1anclem6  38272  ftc1anclem7  38273  ftc1anclem8  38274  dvasin  38278  dvacos  38279  dvreasin  38280  dvreacos  38281  areacirclem1  38282  areacirc  38287  fsumshftd  39651  hlrelat5N  40100  rhmzrhval  42664  aks6d1c1  42808  hashscontpow  42814  aks6d1c4  42816  aks6d1c2lem3  42818  aks6d1c2lem4  42819  aks6d1c2  42822  aks6d1c5lem0  42827  aks6d1c5lem3  42829  aks6d1c5lem2  42830  aks6d1c5  42831  sticksstones3  42840  sticksstones8  42845  sticksstones10  42847  sticksstones12a  42849  sticksstones12  42850  aks6d1c6lem1  42862  aks6d1c6lem2  42863  aks6d1c6lem3  42864  aks6d1c6lem4  42865  aks6d1c6isolem1  42866  aks6d1c6isolem2  42867  aks6d1c6isolem3  42868  aks6d1c6lem5  42869  aks6d1c7lem2  42873  unitscyglem1  42887  readvrec2  43047  readvrec  43048  readvcot  43050  frlmfzolen  43202  frlmfzoccat  43204  frlmvscadiccat  43205  evlsbagval  43245  evlselv  43248  fsuppind  43249  mhpind  43253  mhphflem  43255  prjspner  43278  prjspnvs  43279  prjspnfv01  43283  prjspner01  43284  prjspner1  43285  0prjspnrel  43286  prjcrv0  43292  mzpclall  43385  mzpsubst  43406  eldioph2  43420  rabdiophlem2  43456  irrapxlem1  43476  mzpcong  43626  mendlmod  43843  naddcnff  44016  relexpmulnn  44362  iunrelexpuztr  44372  mnringvald  44864  mnringmulrvald  44878  radcnvrat  44951  hashnzfzclim  44959  lhe4.4ex1a  44966  expgrowthi  44970  expgrowth  44972  bccval  44975  binomcxplemrat  44987  binomcxplemfrat  44988  binomcxplemradcnv  44989  binomcxplemdvbinom  44990  binomcxplemdvsum  44992  binomcxplemnotnn0  44993  unirnmap  45851  unirnmapsn  45857  ssmapsn  45859  iocopn  46163  icoopn  46168  divcnvg  46270  sumnnodd  46273  climsubmpt  46301  dvsinax  46554  fperdvper  46560  dvdivf  46563  dvnprodlem1  46587  itgsincmulx  46615  stoweidlem59  46700  etransclem4  46879  etransclem13  46888  etransclem25  46900  etransclem48  46923  rrxtopnfi  46928  sge0tsms  47021  elhoi  47183  ovnval2  47186  ovnval2b  47193  ovncvrrp  47205  ovn0lem  47206  ovncl  47208  ovnome  47214  hoidmvlelem2  47237  hoidmvlelem3  47238  hoidmvle  47241  ovnlecvr2  47251  ovncvr2  47252  ovnsubadd2lem  47286  ovnovollem1  47297  vonvolmbl  47302  iunhoiioolem  47316  vonioolem1  47321  vonioolem2  47322  vonicclem2  47325  smfresal  47429  smfres  47431  smfmullem4  47435  smfco  47443  adddmmbl  47474  muldmmbl  47476  chnsuslle  47524  nthrucw  47529  sinnpoly  47552  fmtno  48205  isubgruhgr  48557  grtriprop  48630  grtriclwlk3  48634  gpgvtx  48732  gpgiedg  48733  intopval  48891  clintopval  48893  rngchomALTV  48957  funcringcsetcALTV2lem5  48983  ringchomALTV  48991  funcringcsetclem5ALTV  49006  srhmsubcALTVlem2  49013  srhmsubcALTV  49014  fldhmsubcALTV  49022  zlmodzxzscm  49057  zlmodzxzadd  49058  rmsupp0  49068  domnmsuppn0  49069  rmsuppss  49070  ply1mulgsumlem3  49088  ply1mulgsumlem4  49089  ply1mulgsum  49090  dmatALTval  49100  lincop  49108  lincval  49109  linc1  49125  lincresunit3lem1  49179  fdivmpt  49240  fdivmptfv  49245  refdivmptfv  49246  digval  49298  2arymptfv  49350  2arymaptfo  49354  itcovalpclem1  49370  itcovalt2lem1  49375  ackvalsuc1mpt  49378  ackval1  49381  ackval2  49382  ackval3  49383  ackval42  49396  line2xlem  49453  upfval2  49875  swapfval  49960  tposcurf1  49997  tposcurf2val  49999  fucofvalg  50016  fuco112x  50030  fuco23  50039  fucoid  50046  fucocolem4  50054  prcofvalg  50074  prcof1  50086  opf2fval  50103  lanval  50317  ranval  50318