Theorem ovexd 7439

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

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

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 5305

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 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908  df-iota 6492  df-fv 6548  df-ov 7407

This theorem is referenced by:  caofass  7702  caofdi  7704  caofdir  7705  caonncan  7706  suppofssd  8183  mapsnend  9032  snmapen  9034  pw2eng  9074  mapen  9137  mapxpen  9139  mapunen  9142  mapdom2  9144  cantnfcl  9658  cantnfle  9662  cantnflt  9663  cantnflt2  9664  cantnfp1lem2  9670  cantnfp1lem3  9671  cantnflem1b  9677  cantnflem1d  9679  cantnflem1  9680  cnfcomlem  9690  cnfcom  9691  cnfcom2lem  9692  cnfcom3lem  9694  fzen  13514  seqf1o  14005  wrdexg  14470  wrdnval  14491  pfxval  14619  pfxswrd  14652  splval  14697  cshwsexaOLD  14771  ofccat  14912  climshftlem  15514  climshft  15516  climshft2  15522  caucvgr  15618  fsumrev  15721  hashdvds  16704  setsabs  17108  ressress  17189  firest  17374  prdsvscafval  17422  qusval  17484  xpsbas  17514  xpsadd  17516  xpsmul  17517  xpssca  17518  xpsvsca  17519  xpsless  17520  xpsle  17521  homfval  17632  comfval  17640  cicfval  17740  rescabs  17778  rescabsOLD  17779  rescabs2  17780  resscat  17798  funcres2c  17848  ressffth  17885  fucbas  17908  fuccoval  17912  setchom  18026  catchom  18049  catcco  18051  estrchom  18074  funcestrcsetclem5  18092  funcsetcestrclem5  18107  evlf2val  18168  curf11  18175  curf12  18176  curf2val  18179  uncfval  18183  diagval  18189  hof2  18206  yonval  18210  gsumval2a  18600  gsumval2  18601  gsumwspan  18723  efmnd  18747  orbstafun  19169  orbstaval  19170  symgval  19229  psgnvalii  19370  lsmhash  19566  frgpupval  19635  qusabl  19725  gsumval3  19767  gsumreidx  19777  gsumzaddlem  19781  gsummptshft  19796  telgsumfzslem  19848  telgsumfz  19850  telgsumfz0  19852  dpjval  19918  srgbinomlem3  20042  srgbinomlem4  20043  mulgass3  20156  lcomfsupp  20500  rmodislmodlem  20527  rmodislmod  20528  rmodislmodOLD  20529  sraval  20777  srasca  20786  srascaOLD  20787  crngridl  20863  quscrng  20865  znval  21071  znzrhfo  21087  znunithash  21104  cygznlem2  21108  pjfval  21245  pjpm  21247  frlmgsum  21311  frlmipval  21318  frlmphllem  21319  frlmphl  21320  frlmsslsp  21335  frlmup1  21337  gsumbagdiaglemOLD  21473  psrass1lemOLD  21475  gsumbagdiaglem  21476  psrass1lem  21478  psrass1  21507  psrdi  21508  psrdir  21509  psrass23l  21510  mplval  21530  mplsubglem  21540  mplsubrglem  21545  mplmonmul  21573  mplcoe1  21574  opsrval  21583  psrbagev1  21620  psrbagev1OLD  21621  psrbagev2  21622  evlslem6  21626  evlslem1  21627  evlsval  21631  mpfconst  21646  mpff  21649  mpfaddcl  21650  mpfmulcl  21651  mpfind  21652  mhpmulcl  21674  mhpaddcl  21676  mhpvscacl  21679  ply1lss  21702  gsumply1subr  21738  coe1add  21768  coe1tm  21777  coe1tmmul  21781  cply1mul  21800  ply1coe  21802  evl1expd  21846  pf1mpf  21853  pf1ind  21856  mamufv  21871  mamuass  21884  mamuvs1  21887  mamuvs2  21888  matgsum  21921  dmatmul  21981  scmatval  21988  scmatrhmval  22011  mvmulfv  22028  mavmulfv  22030  mavmulass  22033  marrepeval  22047  marepveval  22052  submaeval  22066  mdetrsca  22087  mdetunilem9  22104  mdetuni0  22105  gsummatr01lem3  22141  gsummatr01lem4  22142  gsummatr01  22143  smadiadetlem3  22152  cramerlem1  22171  mat2pmatmul  22215  m2cpminvid  22237  decpmatfsupp  22253  decpmatmullem  22255  decpmatmul  22256  decpmatmulsumfsupp  22257  pmatcollpw1lem1  22258  pmatcollpw3fi1lem1  22270  pmatcollpwscmatlem2  22274  pm2mpfval  22280  pm2mpf  22282  mply1topmatcllem  22287  mp2pm2mplem3  22292  mp2pm2mplem4  22293  pm2mpmhmlem1  22302  pm2mpmhmlem2  22303  pm2mp  22309  chfacfscmulfsupp  22343  chfacfscmulgsum  22344  chfacfpmmulfsupp  22347  chfacfpmmulgsum  22348  cpmidpmatlem3  22356  cpmadugsumlemB  22358  cpmadugsumlemC  22359  cpmadugsumlemF  22360  cayhamlem4  22372  xpstopnlem2  23297  fcfval  23519  tsmsxplem1  23639  tsmsxplem2  23640  tusval  23752  xpsdsfn  23865  xpsxmet  23868  xpsdsval  23869  xpsmet  23870  tmsval  23971  met1stc  24012  metuval  24040  cnmpopc  24426  pi1val  24535  pi1addf  24545  pi1addval  24546  pi1grplem  24547  rrxnm  24890  rrxcph  24891  rrxmval  24904  mbfmulc2  25162  mbfmul  25226  itg2mulclem  25246  ibladd  25320  itgadd  25324  itgabs  25334  bddmulibl  25338  dvmulf  25442  dvcmulf  25444  dvmptmul  25460  dvlip  25492  ftc1lem4  25538  mdegmullem  25578  coe1mul3  25599  r1pval  25656  plyco  25737  dgrcolem1  25769  elqaalem3  25816  taylpfval  25859  taylthlem2  25868  pserdvlem2  25922  advlogexp  26145  logtayl  26150  logccv  26153  dvcxp1  26228  dvcncxp1  26231  logbmpt  26273  logbfval  26275  relogbf  26276  dvatan  26420  cxp2lim  26461  cxploglim2  26463  lgamgulmlem2  26514  lgamgulm2  26520  lgamcvglem  26524  lgamf  26526  basellem7  26571  basellem8  26572  basellem9  26573  fsumdvdscom  26669  logexprlim  26708  dchrfi  26738  gausslemma2dlem2  26850  gausslemma2dlem3  26851  2lgslem1b  26875  chtppilimlem2  26957  chebbnd2  26960  chto1lb  26961  chpchtlim  26962  chpo1ub  26963  vmadivsum  26965  dchrisum0lem3  27002  mudivsum  27013  logdivsum  27016  log2sumbnd  27027  selberglem1  27028  selberg2lem  27033  selberg2  27034  selbergr  27051  negsval  27480  wlkp1  28918  wwlksnextsurj  29134  wwlksnextbij  29136  clwlkclwwlklem2a1  29225  clwlkclwwlkf1  29243  eupth2eucrct  29450  frgrncvvdeq  29542  numclwlk2lem2fv  29611  numclwwlk2lem3  29613  ofoprabco  31867  fsuppcurry1  31928  fsuppcurry2  31929  offinsupp1  31930  ressprs  32111  resspos  32114  mntoval  32130  mgcoval  32134  lmodvslmhm  32180  cycpmco2f1  32261  cycpmco2rn  32262  cycpmco2lem2  32264  cycpmco2lem3  32265  cycpmco2lem4  32266  cycpmco2lem5  32267  cycpmco2lem6  32268  cycpmco2  32270  archirngz  32313  archiabllem2a  32318  frobrhm  32357  quslmod  32438  quslmhm  32439  quslvec  32440  qustriv  32445  qustrivr  32446  nsgmgc  32486  nsgqusf1olem1  32487  nsgqusf1olem2  32488  nsgqusf1olem3  32489  ghmquskerlem1  32491  ghmquskerco  32492  ghmquskerlem2  32493  ghmqusker  32494  lmhmqusker  32496  rhmqusker  32502  elrspunidl  32504  qsidomlem1  32529  qsidomlem2  32530  opprqusbas  32555  opprqusplusg  32556  opprqusmulr  32558  opprqus1r  32559  qsdrngilem  32561  qsdrngi  32562  ply1gsumz  32616  ply1degltdimlem  32652  ply1degltdim  32653  qusdimsum  32658  fedgmullem1  32659  fedgmullem2  32660  fedgmul  32661  submateq  32727  lmatcl  32734  mdetpmtr1  32741  madjusmdetlem1  32745  madjusmdetlem3  32747  qqhvval  32901  esumfzf  33005  esumpfinvallem  33010  esumpmono  33015  esummulc1  33017  esumcvg  33022  esumgect  33026  ofcval  33035  omssubadd  33237  sitgfval  33278  sitmcl  33288  sseqfv2  33331  cndprobval  33370  ballotlemfval  33426  ballotlemsv  33446  ballotlemsf1o  33450  ofcccat  33492  signsplypnf  33499  signsply0  33500  signstfval  33513  signshf  33537  reprpmtf1o  33576  reprdifc  33577  logdivsqrle  33600  hgt750lemg  33604  hgt750lema  33607  lpadval  33626  cvmliftlem8  34221  cvmliftphtlem  34246  fmla1  34316  gonarlem  34323  sategoelfvb  34348  mrsubval  34438  fwddifval  35072  gg-cmvth  35119  knoppcnlem1  35307  knoppcnlem6  35312  unbdqndv2lem2  35324  poimirlem1  36427  poimirlem2  36428  poimirlem3  36429  poimirlem5  36431  poimirlem6  36432  poimirlem7  36433  poimirlem10  36436  poimirlem11  36437  poimirlem12  36438  poimirlem16  36442  poimirlem19  36445  poimirlem22  36448  poimirlem23  36449  broucube  36460  dvtan  36476  itg2addnc  36480  ibladdnc  36483  itgaddnc  36486  itgmulc2nclem2  36493  itgmulc2nc  36494  itgabsnc  36495  ftc1cnnclem  36497  ftc1anclem3  36501  ftc1anclem6  36504  ftc1anclem7  36505  ftc1anclem8  36506  dvasin  36510  dvacos  36511  dvreasin  36512  dvreacos  36513  areacirclem1  36514  areacirc  36519  fsumshftd  37760  hlrelat5N  38210  sticksstones3  40902  sticksstones8  40907  sticksstones10  40909  sticksstones12a  40911  sticksstones12  40912  frlmfzolen  41026  frlmfzoccat  41028  frlmvscadiccat  41029  rhmmpllem1  41071  rhmmpl  41075  evlscl  41080  evlsval3  41081  evlsvval  41082  evlsvvval  41085  evlsbagval  41088  evlsexpval  41089  evlsaddval  41090  evlsmulval  41091  evlsevl  41093  evlcl  41094  evladdval  41097  evlmulval  41098  selvcl  41105  evlselv  41109  fsuppind  41112  mhpind  41116  mhphflem  41118  prjspner  41305  prjspnvs  41306  prjspnfv01  41310  prjspner01  41311  prjspner1  41312  0prjspnrel  41313  prjcrv0  41319  mzpclall  41398  mzpsubst  41419  eldioph2  41433  rabdiophlem2  41473  irrapxlem1  41493  mzpcong  41644  mendlmod  41868  naddcnff  42045  relexpmulnn  42393  iunrelexpuztr  42403  mnringvald  42900  mnringmulrvald  42919  radcnvrat  43006  hashnzfzclim  43014  lhe4.4ex1a  43021  expgrowthi  43025  expgrowth  43027  bccval  43030  binomcxplemrat  43042  binomcxplemfrat  43043  binomcxplemradcnv  43044  binomcxplemdvbinom  43045  binomcxplemdvsum  43047  binomcxplemnotnn0  43048  unirnmap  43840  unirnmapsn  43846  ssmapsn  43848  iocopn  44168  icoopn  44173  divcnvg  44278  sumnnodd  44281  climsubmpt  44311  dvsinax  44564  fperdvper  44570  dvdivf  44573  dvnprodlem1  44597  itgsincmulx  44625  stoweidlem59  44710  etransclem4  44889  etransclem13  44898  etransclem25  44910  etransclem48  44933  rrxtopnfi  44938  sge0tsms  45031  elhoi  45193  ovnval2  45196  ovnval2b  45203  ovncvrrp  45215  ovn0lem  45216  ovncl  45218  ovnome  45224  hoidmvlelem2  45247  hoidmvlelem3  45248  hoidmvle  45251  ovnlecvr2  45261  ovncvr2  45262  ovnsubadd2lem  45296  ovnovollem1  45307  vonvolmbl  45312  iunhoiioolem  45326  vonioolem1  45331  vonioolem2  45332  vonicclem2  45335  smfresal  45439  smfres  45441  smfmullem4  45445  smfco  45453  adddmmbl  45484  muldmmbl  45486  fmtno  46132  intopval  46547  clintopval  46549  prdsrngd  46612  rngcval  46762  rnghmsscmap2  46773  rnghmsscmap  46774  rngchomALTV  46785  funcrngcsetc  46798  ringcval  46808  rhmsscmap2  46819  rhmsscmap  46820  funcringcsetc  46835  funcringcsetcALTV2lem5  46840  ringchomALTV  46848  funcringcsetclem5ALTV  46863  srhmsubclem3  46875  srhmsubc  46876  fldhmsubc  46884  srhmsubcALTVlem2  46893  srhmsubcALTV  46894  fldhmsubcALTV  46902  zlmodzxzscm  46935  zlmodzxzadd  46936  rmsupp0  46946  domnmsuppn0  46947  rmsuppss  46948  mndpsuppss  46949  ply1mulgsumlem3  46971  ply1mulgsumlem4  46972  ply1mulgsum  46973  dmatALTval  46983  lincop  46991  lincval  46992  linc1  47008  lincresunit3lem1  47062  fdivmpt  47128  fdivmptfv  47133  refdivmptfv  47134  digval  47186  2arymptfv  47238  2arymaptfo  47242  itcovalpclem1  47258  itcovalt2lem1  47263  ackvalsuc1mpt  47266  ackval1  47269  ackval2  47270  ackval3  47271  ackval42  47284  line2xlem  47341