Theorem ovexd 6680

Description: The result of an operation is a set (common case). (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Assertion

Ref	Expression
ovexd	⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Proof of Theorem ovexd

Step	Hyp	Ref	Expression
1		ovex 6678	. 2 ⊢ (𝐴𝐹𝐵) ∈ V
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  caofass  6931  caofdi  6933  caofdir  6934  caonncan  6935  map1  8036  pw2eng  8066  mapen  8124  mapxpen  8126  mapdom2  8131  cantnfcl  8564  cantnflem1  8586  cnfcomlem  8596  cnfcom3lem  8600  cda1dif  8998  fzen  12358  seqf1o  12842  wrdnval  13335  splval  13502  cshwsexa  13570  ofccat  13708  climshftlem  14305  climshft  14307  climshft2  14313  caucvgr  14406  hashdvds  15480  setsabs  15902  ressress  15938  prdsvscafval  16140  qusval  16202  xpsbas  16234  xpsadd  16236  xpsmul  16237  xpssca  16238  xpsvsca  16239  xpsless  16240  xpsle  16241  homfval  16352  comfval  16360  cicfval  16457  rescabs  16493  rescabs2  16494  resscat  16512  fucbas  16620  fuccoval  16623  setchom  16730  catchom  16749  catcco  16751  estrchom  16767  funcestrcsetclem5  16784  funcsetcestrclem5  16799  evlf2val  16859  curf11  16866  curf12  16867  curf2val  16870  uncfval  16874  diagval  16880  hof2  16897  yonval  16901  gsumval2a  17279  gsumval2  17280  gsumwspan  17383  orbstafun  17744  orbstaval  17745  psgnvalii  17929  lsmhash  18118  frgpupval  18187  qusabl  18268  gsumval3  18308  gsumzaddlem  18321  gsummptshft  18336  telgsumfzslem  18385  telgsumfz  18387  telgsumfz0  18389  dpjval  18455  srgbinomlem3  18542  srgbinomlem4  18543  mulgass3  18637  lcomfsupp  18903  rmodislmodlem  18930  rmodislmod  18931  sraval  19176  srasca  19181  crngridl  19238  quscrng  19240  gsumbagdiaglem  19375  psrass1lem  19377  psrass1  19405  psrdi  19406  psrdir  19407  psrass23l  19408  mplval  19428  mplsubglem  19434  mplsubrglem  19439  mplmonmul  19464  mplcoe1  19465  opsrval  19474  psrbagev1  19510  evlslem6  19513  evlslem1  19515  evlsval  19519  mpfconst  19530  mpff  19533  mpfaddcl  19534  mpfmulcl  19535  mpfind  19536  ply1lss  19566  gsumply1subr  19604  coe1add  19634  coe1tm  19643  coe1tmmul  19647  cply1mul  19664  ply1coe  19666  evl1expd  19709  pf1mpf  19716  pf1ind  19719  znval  19883  znzrhfo  19896  znunithash  19913  cygznlem2  19917  pjfval  20050  pjpm  20052  frlmgsum  20111  frlmipval  20118  frlmphllem  20119  frlmphl  20120  frlmsslsp  20135  mamufv  20193  mamuass  20208  mamuvs1  20211  mamuvs2  20212  matgsum  20243  dmatmul  20303  scmatval  20310  scmatrhmval  20333  mvmulfv  20350  mavmulfv  20352  mavmulass  20355  marrepeval  20369  marepveval  20374  submaeval  20388  mdetrsca  20409  mdetunilem9  20426  mdetuni0  20427  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  smadiadetlem3  20474  cramerlem1  20493  mat2pmatmul  20536  m2cpminvid  20558  decpmatfsupp  20574  decpmatmullem  20576  decpmatmul  20577  decpmatmulsumfsupp  20578  pmatcollpw1lem1  20579  pmatcollpw3fi1lem1  20591  pmatcollpwscmatlem2  20595  pm2mpfval  20601  pm2mpf  20603  mply1topmatcllem  20608  mp2pm2mplem3  20613  mp2pm2mplem4  20614  pm2mpmhmlem1  20623  pm2mpmhmlem2  20624  pm2mp  20630  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  cpmidpmatlem3  20677  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cayhamlem4  20693  xpstopnlem2  21614  fcfval  21837  tsmsxplem1  21956  tsmsxplem2  21957  tusval  22070  xpsdsfn  22182  xpsxmet  22185  xpsdsval  22186  xpsmet  22187  tmsval  22286  met1stc  22326  metuval  22354  cnmpt2pc  22727  pi1val  22837  pi1addf  22847  pi1addval  22848  pi1grplem  22849  rrxnm  23179  rrxcph  23180  rrxmval  23188  mbfmulc2  23430  mbfmul  23493  itg2mulclem  23513  ibladd  23587  itgadd  23591  itgabs  23601  bddmulibl  23605  dvmulf  23706  dvcmulf  23708  dvmptmul  23724  dvlip  23756  ftc1lem4  23802  mdegmullem  23838  coe1mul3  23859  r1pval  23916  plyco  23997  dgrcolem1  24029  elqaalem3  24076  taylpfval  24119  taylthlem2  24128  pserdvlem2  24182  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvcncxp1  24484  logbmpt  24526  logbfval  24528  relogbf  24529  dvatan  24662  cxp2lim  24703  cxploglim2  24705  lgamgulmlem2  24756  lgamgulm2  24762  lgamcvglem  24766  lgamf  24768  basellem7  24813  basellem8  24814  basellem9  24815  fsumdvdscom  24911  logexprlim  24950  dchrfi  24980  gausslemma2dlem2  25092  gausslemma2dlem3  25093  2lgslem1b  25117  chtppilimlem2  25163  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  vmadivsum  25171  dchrisum0lem3  25208  mudivsum  25219  logdivsum  25222  log2sumbnd  25233  selberglem1  25234  selberg2lem  25239  selberg2  25240  selbergr  25257  wlkp1  26578  wwlksnextsur  26795  wwlksnextbij  26797  clwlkclwwlklem2a1  26893  eupth2eucrct  27077  frgrncvvdeq  27173  numclwlk2lem2fv  27237  numclwwlk2lem3  27239  ofoprabco  29464  ressprs  29655  resspos  29659  archirngz  29743  archiabllem2a  29748  submateq  29875  lmatcl  29882  mdetpmtr1  29889  madjusmdetlem1  29893  madjusmdetlem3  29895  qqhvval  30027  esumfzf  30131  esumpfinvallem  30136  esumpmono  30141  esummulc1  30143  esumcvg  30148  esumgect  30152  ofcval  30161  omssubadd  30362  sitgfval  30403  sitmcl  30413  sseqfv2  30456  cndprobval  30495  ballotlemfval  30551  ballotlemsv  30571  ballotlemsf1o  30575  ofcccat  30620  signsplypnf  30627  signsply0  30628  signstfval  30641  signshf  30665  reprpmtf1o  30704  reprdifc  30705  logdivsqrle  30728  hgt750lemg  30732  hgt750lema  30735  cvmliftlem8  31274  cvmliftphtlem  31299  mrsubval  31406  fwddifval  32269  knoppcnlem1  32483  knoppcnlem6  32488  unbdqndv2lem2  32501  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem19  33428  poimirlem22  33431  poimirlem23  33432  broucube  33443  dvtan  33460  itg2addnc  33464  ibladdnc  33467  itgaddnc  33470  itgmulc2nclem2  33477  itgmulc2nc  33478  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem3  33487  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  areacirclem1  33500  areacirc  33505  fsumshftd  34237  hlrelat5N  34687  mzpclall  37290  mzpsubst  37311  eldioph2  37325  rabdiophlem2  37366  irrapxlem1  37386  mzpcong  37539  mendlmod  37763  relexpmulnn  38001  iunrelexpuztr  38011  radcnvrat  38513  hashnzfzclim  38521  lhe4.4ex1a  38528  expgrowthi  38532  expgrowth  38534  bccval  38537  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemradcnv  38551  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  mapsnend  39391  unirnmap  39400  unirnmapsn  39406  ssmapsn  39408  iocopn  39746  icoopn  39751  divcnvg  39859  sumnnodd  39862  climsubmpt  39892  dvsinax  40127  fperdvper  40133  dvdivf  40137  dvnprodlem1  40161  itgsincmulx  40190  stoweidlem59  40276  etransclem4  40455  etransclem13  40464  etransclem25  40476  etransclem48  40499  rrxtopnfi  40506  sge0tsms  40597  elhoi  40756  ovnval2  40759  ovnval2b  40766  ovncvrrp  40778  ovn0lem  40779  ovncl  40781  ovnome  40787  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvle  40814  ovnlecvr2  40824  ovncvr2  40825  ovnsubadd2lem  40859  ovnovollem1  40870  vonvolmbl  40875  iunhoiioolem  40889  vonioolem1  40894  vonioolem2  40895  vonicclem2  40898  smfresal  40995  smfres  40997  smfmullem4  41001  smfco  41009  pfxval  41383  fmtno  41441  intopval  41838  clintopval  41840  rngcval  41962  rnghmsscmap2  41973  rnghmsscmap  41974  rngchomALTV  41985  funcrngcsetc  41998  ringcval  42008  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetc  42035  funcringcsetcALTV2lem5  42040  ringchomALTV  42048  funcringcsetclem5ALTV  42063  srhmsubclem3  42075  srhmsubc  42076  fldhmsubc  42084  srhmsubcALTVlem2  42093  srhmsubcALTV  42094  fldhmsubcALTV  42102  zlmodzxzscm  42135  zlmodzxzadd  42136  rmsupp0  42149  domnmsuppn0  42150  rmsuppss  42151  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  ply1mulgsum  42178  dmatALTval  42189  lincop  42197  lincval  42198  linc1  42214  lincresunit3lem1  42268  fdivmpt  42334  fdivmptfv  42339  refdivmptfv  42340  digval  42392