Theorem ovexd 7194

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3497  (class class class)co 7159

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-nul 5213

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-sn 4571  df-pr 4573  df-uni 4842  df-iota 6317  df-fv 6366  df-ov 7162

This theorem is referenced by:  caofass  7446  caofdi  7448  caofdir  7449  caonncan  7450  suppofssd  7870  mapsnend  8591  snmapen  8593  pw2eng  8626  mapen  8684  mapxpen  8686  mapdom2  8691  cantnfcl  9133  cantnfle  9137  cantnflt  9138  cantnflt2  9139  cantnfp1lem2  9145  cantnfp1lem3  9146  cantnflem1b  9152  cantnflem1d  9154  cantnflem1  9155  cnfcomlem  9165  cnfcom  9166  cnfcom2lem  9167  cnfcom3lem  9169  fzen  12927  seqf1o  13414  wrdexg  13874  wrdnval  13899  pfxval  14038  pfxswrd  14071  splval  14116  cshwsexa  14189  ofccat  14332  climshftlem  14934  climshft  14936  climshft2  14942  caucvgr  15035  fsumrev  15137  hashdvds  16115  setsabs  16529  ressress  16565  firest  16709  prdsvscafval  16756  qusval  16818  xpsbas  16848  xpsadd  16850  xpsmul  16851  xpssca  16852  xpsvsca  16853  xpsless  16854  xpsle  16855  homfval  16965  comfval  16973  cicfval  17070  rescabs  17106  rescabs2  17107  resscat  17125  funcres2c  17174  ressffth  17211  fucbas  17233  fuccoval  17236  setchom  17343  catchom  17362  catcco  17364  estrchom  17380  funcestrcsetclem5  17397  funcsetcestrclem5  17412  evlf2val  17472  curf11  17479  curf12  17480  curf2val  17483  uncfval  17487  diagval  17493  hof2  17510  yonval  17514  gsumval2a  17898  gsumval2  17899  gsumwspan  18014  efmnd  18038  orbstafun  18444  orbstaval  18445  symgval  18500  psgnvalii  18640  lsmhash  18834  frgpupval  18903  qusabl  18988  gsumval3  19030  gsumreidx  19040  gsumzaddlem  19044  gsummptshft  19059  telgsumfzslem  19111  telgsumfz  19113  telgsumfz0  19115  dpjval  19181  srgbinomlem3  19295  srgbinomlem4  19296  mulgass3  19390  lcomfsupp  19677  rmodislmodlem  19704  rmodislmod  19705  sraval  19951  srasca  19956  crngridl  20014  quscrng  20016  gsumbagdiaglem  20158  psrass1lem  20160  psrass1  20188  psrdi  20189  psrdir  20190  psrass23l  20191  mplval  20211  mplsubglem  20217  mplsubrglem  20222  mplmonmul  20248  mplcoe1  20249  opsrval  20258  psrbagev1  20293  evlslem6  20297  evlslem1  20298  evlsval  20302  mpfconst  20317  mpff  20320  mpfaddcl  20321  mpfmulcl  20322  mpfind  20323  mhpaddcl  20341  mhpinvcl  20342  mhpvscacl  20344  ply1lss  20367  gsumply1subr  20405  coe1add  20435  coe1tm  20444  coe1tmmul  20448  cply1mul  20465  ply1coe  20467  evl1expd  20511  pf1mpf  20518  pf1ind  20521  znval  20685  znzrhfo  20697  znunithash  20714  cygznlem2  20718  pjfval  20853  pjpm  20855  frlmgsum  20919  frlmipval  20926  frlmphllem  20927  frlmphl  20928  frlmsslsp  20943  frlmup1  20945  mamufv  21001  mamuass  21014  mamuvs1  21017  mamuvs2  21018  matgsum  21049  dmatmul  21109  scmatval  21116  scmatrhmval  21139  mvmulfv  21156  mavmulfv  21158  mavmulass  21161  marrepeval  21175  marepveval  21180  submaeval  21194  mdetrsca  21215  mdetunilem9  21232  mdetuni0  21233  gsummatr01lem3  21269  gsummatr01lem4  21270  gsummatr01  21271  smadiadetlem3  21280  cramerlem1  21299  mat2pmatmul  21342  m2cpminvid  21364  decpmatfsupp  21380  decpmatmullem  21382  decpmatmul  21383  decpmatmulsumfsupp  21384  pmatcollpw1lem1  21385  pmatcollpw3fi1lem1  21397  pmatcollpwscmatlem2  21401  pm2mpfval  21407  pm2mpf  21409  mply1topmatcllem  21414  mp2pm2mplem3  21419  mp2pm2mplem4  21420  pm2mpmhmlem1  21429  pm2mpmhmlem2  21430  pm2mp  21436  chfacfscmulfsupp  21470  chfacfscmulgsum  21471  chfacfpmmulfsupp  21474  chfacfpmmulgsum  21475  cpmidpmatlem3  21483  cpmadugsumlemB  21485  cpmadugsumlemC  21486  cpmadugsumlemF  21487  cayhamlem4  21499  xpstopnlem2  22422  fcfval  22644  tsmsxplem1  22764  tsmsxplem2  22765  tusval  22878  xpsdsfn  22990  xpsxmet  22993  xpsdsval  22994  xpsmet  22995  tmsval  23094  met1stc  23134  metuval  23162  cnmpopc  23535  pi1val  23644  pi1addf  23654  pi1addval  23655  pi1grplem  23656  rrxnm  23997  rrxcph  23998  rrxmval  24011  mbfmulc2  24267  mbfmul  24330  itg2mulclem  24350  ibladd  24424  itgadd  24428  itgabs  24438  bddmulibl  24442  dvmulf  24543  dvcmulf  24545  dvmptmul  24561  dvlip  24593  ftc1lem4  24639  mdegmullem  24675  coe1mul3  24696  r1pval  24753  plyco  24834  dgrcolem1  24866  elqaalem3  24913  taylpfval  24956  taylthlem2  24965  pserdvlem2  25019  advlogexp  25241  logtayl  25246  logccv  25249  dvcxp1  25324  dvcncxp1  25327  logbmpt  25369  logbfval  25371  relogbf  25372  dvatan  25516  cxp2lim  25557  cxploglim2  25559  lgamgulmlem2  25610  lgamgulm2  25616  lgamcvglem  25620  lgamf  25622  basellem7  25667  basellem8  25668  basellem9  25669  fsumdvdscom  25765  logexprlim  25804  dchrfi  25834  gausslemma2dlem2  25946  gausslemma2dlem3  25947  2lgslem1b  25971  chtppilimlem2  26053  chebbnd2  26056  chto1lb  26057  chpchtlim  26058  chpo1ub  26059  vmadivsum  26061  dchrisum0lem3  26098  mudivsum  26109  logdivsum  26112  log2sumbnd  26123  selberglem1  26124  selberg2lem  26129  selberg2  26130  selbergr  26147  wlkp1  27466  wwlksnextsurj  27681  wwlksnextbij  27683  clwlkclwwlklem2a1  27773  clwlkclwwlkf1  27791  eupth2eucrct  27999  frgrncvvdeq  28091  numclwlk2lem2fv  28160  numclwwlk2lem3  28162  ofoprabco  30412  fsuppcurry1  30464  fsuppcurry2  30465  offinsupp1  30466  ressprs  30646  resspos  30650  lmodvslmhm  30692  cycpmco2f1  30770  cycpmco2rn  30771  cycpmco2lem2  30773  cycpmco2lem3  30774  cycpmco2lem4  30775  cycpmco2lem5  30776  cycpmco2lem6  30777  cycpmco2  30779  archirngz  30822  archiabllem2a  30827  quslmod  30927  quslmhm  30928  qustriv  30933  qustrivr  30934  qsidomlem1  30969  qsidomlem2  30970  qusdimsum  31028  fedgmullem1  31029  fedgmullem2  31030  fedgmul  31031  submateq  31078  lmatcl  31085  mdetpmtr1  31092  madjusmdetlem1  31096  madjusmdetlem3  31098  qqhvval  31228  esumfzf  31332  esumpfinvallem  31337  esumpmono  31342  esummulc1  31344  esumcvg  31349  esumgect  31353  ofcval  31362  omssubadd  31562  sitgfval  31603  sitmcl  31613  sseqfv2  31656  cndprobval  31695  ballotlemfval  31751  ballotlemsv  31771  ballotlemsf1o  31775  ofcccat  31817  signsplypnf  31824  signsply0  31825  signstfval  31838  signshf  31862  reprpmtf1o  31901  reprdifc  31902  logdivsqrle  31925  hgt750lemg  31929  hgt750lema  31932  lpadval  31951  cvmliftlem8  32543  cvmliftphtlem  32568  fmla1  32638  gonarlem  32645  sategoelfvb  32670  mrsubval  32760  fwddifval  33627  knoppcnlem1  33836  knoppcnlem6  33841  unbdqndv2lem2  33853  poimirlem1  34897  poimirlem2  34898  poimirlem3  34899  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem10  34906  poimirlem11  34907  poimirlem12  34908  poimirlem16  34912  poimirlem19  34915  poimirlem22  34918  poimirlem23  34919  broucube  34930  dvtan  34946  itg2addnc  34950  ibladdnc  34953  itgaddnc  34956  itgmulc2nclem2  34963  itgmulc2nc  34964  itgabsnc  34965  ftc1cnnclem  34969  ftc1anclem3  34973  ftc1anclem6  34976  ftc1anclem7  34977  ftc1anclem8  34978  dvasin  34982  dvacos  34983  dvreasin  34984  dvreacos  34985  areacirclem1  34986  areacirc  34991  fsumshftd  36092  hlrelat5N  36541  selvcl  39144  frlmfzolen  39148  frlmfzoccat  39150  frlmvscadiccat  39151  prjspnval2  39273  0prjspnrel  39275  mzpclall  39330  mzpsubst  39351  eldioph2  39365  rabdiophlem2  39405  irrapxlem1  39425  mzpcong  39575  mendlmod  39799  relexpmulnn  40060  iunrelexpuztr  40070  radcnvrat  40652  hashnzfzclim  40660  lhe4.4ex1a  40667  expgrowthi  40671  expgrowth  40673  bccval  40676  binomcxplemrat  40688  binomcxplemfrat  40689  binomcxplemradcnv  40690  binomcxplemdvbinom  40691  binomcxplemdvsum  40693  binomcxplemnotnn0  40694  unirnmap  41477  unirnmapsn  41483  ssmapsn  41485  iocopn  41802  icoopn  41807  divcnvg  41914  sumnnodd  41917  climsubmpt  41947  dvsinax  42203  fperdvper  42209  dvdivf  42213  dvnprodlem1  42237  itgsincmulx  42265  stoweidlem59  42351  etransclem4  42530  etransclem13  42539  etransclem25  42551  etransclem48  42574  rrxtopnfi  42579  sge0tsms  42669  elhoi  42831  ovnval2  42834  ovnval2b  42841  ovncvrrp  42853  ovn0lem  42854  ovncl  42856  ovnome  42862  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvle  42889  ovnlecvr2  42899  ovncvr2  42900  ovnsubadd2lem  42934  ovnovollem1  42945  vonvolmbl  42950  iunhoiioolem  42964  vonioolem1  42969  vonioolem2  42970  vonicclem2  42973  smfresal  43070  smfres  43072  smfmullem4  43076  smfco  43084  fmtno  43698  intopval  44116  clintopval  44118  rngcval  44240  rnghmsscmap2  44251  rnghmsscmap  44252  rngchomALTV  44263  funcrngcsetc  44276  ringcval  44286  rhmsscmap2  44297  rhmsscmap  44298  funcringcsetc  44313  funcringcsetcALTV2lem5  44318  ringchomALTV  44326  funcringcsetclem5ALTV  44341  srhmsubclem3  44353  srhmsubc  44354  fldhmsubc  44362  srhmsubcALTVlem2  44371  srhmsubcALTV  44372  fldhmsubcALTV  44380  zlmodzxzscm  44412  zlmodzxzadd  44413  rmsupp0  44423  domnmsuppn0  44424  rmsuppss  44425  ply1mulgsumlem3  44449  ply1mulgsumlem4  44450  ply1mulgsum  44451  dmatALTval  44462  lincop  44470  lincval  44471  linc1  44487  lincresunit3lem1  44541  fdivmpt  44607  fdivmptfv  44612  refdivmptfv  44613  digval  44665  line2xlem  44747