Theorem ovexd 7447

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-sn 4589  df-pr 4591  df-uni 4872  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  caofidlcan  7714  caofass  7716  caofdi  7718  caofdir  7719  caonncan  7720  suppofssd  8197  mapsnend  9031  snmapen  9033  pw2eng  9069  mapen  9127  mapxpen  9129  mapunen  9132  mapdom2  9134  cantnfcl  9634  cantnfle  9638  cantnflt  9639  cantnflt2  9640  cantnfp1lem2  9646  cantnfp1lem3  9647  cantnflem1b  9653  cantnflem1d  9655  cantnflem1  9656  cnfcomlem  9666  cnfcom  9667  cnfcom2lem  9668  cnfcom3lem  9670  fzen  13575  seqf1o  14086  wrdexg  14568  wrdnval  14589  pfxval  14718  pfxswrd  14750  splval  14795  ofccat  15013  climshftlem  15632  climshft  15634  climshft2  15640  caucvgr  15734  fsumrev  15837  hashdvds  16840  setsabs  17245  ressress  17313  firest  17491  prdsvscafval  17539  qusval  17602  xpsbas  17632  xpsadd  17634  xpsmul  17635  xpssca  17636  xpsvsca  17637  xpsless  17638  xpsle  17639  homfval  17754  comfval  17762  cicfval  17860  rescabs  17896  rescabs2  17897  resscat  17915  funcres2c  17966  ressffth  18003  fucbas  18026  fuccoval  18029  setchom  18143  catchom  18166  catcco  18168  estrchom  18189  funcestrcsetclem5  18206  funcsetcestrclem5  18221  evlf2val  18281  curf11  18288  curf12  18289  curf2val  18292  uncfval  18296  diagval  18302  hof2  18319  yonval  18323  resspos  18491  gsumval2a  18749  gsumval2  18750  mndpsuppss  18829  gsumwspan  18911  efmnd  18935  qustriv  19258  qustrivr  19259  ghmqusnsglem1  19356  ghmqusnsglem2  19357  ghmqusnsg  19358  ghmquskerlem1  19359  ghmquskerco  19360  ghmquskerlem2  19361  ghmquskerlem3  19362  ghmqusker  19363  orbstafun  19387  orbstaval  19388  symgval  19447  psgnvalii  19585  lsmhash  19781  frgpupval  19850  qusabl  19941  gsumval3  19983  gsumreidx  19993  gsumzaddlem  19997  gsummptshft  20012  telgsumfzslem  20064  telgsumfz  20066  telgsumfz0  20068  dpjval  20134  prdsrngd  20260  srgbinomlem3  20316  srgbinomlem4  20317  mulgass3  20442  rngcval  20728  rnghmsscmap2  20739  rnghmsscmap  20740  funcrngcsetc  20750  ringcval  20757  rhmsscmap2  20768  rhmsscmap  20769  funcringcsetc  20784  srhmsubclem3  20789  srhmsubc  20790  fldhmsubc  20899  lcomfsupp  21034  rmodislmodlem  21061  rmodislmod  21062  sraval  21307  srasca  21312  crngridl  21430  quscrng  21434  rhmqusnsg  21436  qsidomlem1  21491  qsidomlem2  21492  pzriprnglem11  21652  znval  21696  znzrhfo  21708  znunithash  21725  cygznlem2  21729  frobrhm  21736  pjfval  21867  pjpm  21869  frlmgsum  21933  frlmipval  21940  frlmphllem  21941  frlmphl  21942  frlmsslsp  21957  frlmup1  21959  gsumbagdiaglem  22092  psrass1lem  22094  rhmpsrlem1  22101  psrass1  22124  psrdi  22125  psrdir  22126  psrass23l  22127  psrascl  22139  mplval  22149  mplsubglem  22159  mplsubrglem  22164  mplmonmul  22198  mplcoe1  22199  opsrval  22208  psrbagev1  22239  psrbagev2  22240  evlslem6  22243  evlslem1  22244  evlsval  22248  evlsval3  22251  evlsvval  22252  evlsvvval  22255  evlcl  22264  evladdval  22265  evlmulval  22266  mpfconst  22271  mpff  22274  mpfaddcl  22275  mpfmulcl  22276  mpfind  22277  mhmcompl  22283  mhmcoaddmpl  22285  evlscl  22287  evlsexpval  22290  evlsaddval  22291  evlsmulval  22292  evlsevl  22294  selvcl  22302  mhpmulcl  22323  mhpaddcl  22325  psdcoef  22334  psdmplcl  22336  psdadd  22337  ply1lss  22367  gsumply1subr  22404  coe1add  22436  coe1tm  22445  coe1tmmul  22449  cply1mul  22467  ply1coe  22469  evl1expd  22516  pf1mpf  22523  pf1ind  22526  rhmmpl  22551  rhmply1vsca  22556  mamufv  22562  mamuass  22570  mamuvs1  22573  mamuvs2  22574  matgsum  22605  dmatmul  22665  scmatval  22672  scmatrhmval  22695  mvmulfv  22712  mavmulfv  22714  mavmulass  22717  marrepeval  22731  marepveval  22736  submaeval  22750  mdetrsca  22771  mdetunilem9  22788  mdetuni0  22789  gsummatr01lem3  22825  gsummatr01lem4  22826  gsummatr01  22827  smadiadetlem3  22836  cramerlem1  22855  mat2pmatmul  22899  m2cpminvid  22921  decpmatfsupp  22937  decpmatmullem  22939  decpmatmul  22940  decpmatmulsumfsupp  22941  pmatcollpw1lem1  22942  pmatcollpw3fi1lem1  22954  pmatcollpwscmatlem2  22958  pm2mpfval  22964  pm2mpf  22966  mply1topmatcllem  22971  mp2pm2mplem3  22976  mp2pm2mplem4  22977  pm2mpmhmlem1  22986  pm2mpmhmlem2  22987  pm2mp  22993  chfacfscmulfsupp  23027  chfacfscmulgsum  23028  chfacfpmmulfsupp  23031  chfacfpmmulgsum  23032  cpmidpmatlem3  23040  cpmadugsumlemB  23042  cpmadugsumlemC  23043  cpmadugsumlemF  23044  cayhamlem4  23056  xpstopnlem2  23979  fcfval  24201  tsmsxplem1  24321  tsmsxplem2  24322  tusval  24433  xpsdsfn  24545  xpsxmet  24548  xpsdsval  24549  xpsmet  24550  tmsval  24649  met1stc  24689  metuval  24717  cnmpopc  25098  pi1val  25207  pi1addf  25217  pi1addval  25218  pi1grplem  25219  rrxnm  25561  rrxcph  25562  rrxmval  25575  mbfmulc2  25833  mbfmul  25896  itg2mulclem  25916  ibladd  25991  itgadd  25995  itgabs  26005  bddmulibl  26009  dvmulf  26113  dvcmulf  26115  dvmptmul  26131  cmvth  26161  dvlip  26163  ftc1lem4  26209  mdegmullem  26246  coe1mul3  26267  r1pval  26326  plyco  26409  dgrcolem1  26441  elqaalem3  26493  taylpfval  26539  taylthlem2  26548  pserdvlem2  26602  advlogexp  26831  logtayl  26836  logccv  26839  dvcxp1  26916  dvcncxp1  26919  logbmpt  26964  logbfval  26966  relogbf  26967  dvatan  27111  cxp2lim  27152  cxploglim2  27154  lgamgulmlem2  27205  lgamgulm2  27211  lgamcvglem  27215  lgamf  27217  basellem7  27262  basellem8  27263  basellem9  27264  fsumdvdscom  27360  logexprlim  27400  dchrfi  27430  gausslemma2dlem2  27542  gausslemma2dlem3  27543  2lgslem1b  27567  chtppilimlem2  27649  chebbnd2  27652  chto1lb  27653  chpchtlim  27654  chpo1ub  27655  vmadivsum  27657  dchrisum0lem3  27694  mudivsum  27705  logdivsum  27708  log2sumbnd  27719  selberglem1  27720  selberg2lem  27725  selberg2  27726  selbergr  27743  negsval  28229  wlkp1  30040  cyclnumvtx  30160  wwlksnextsurj  30260  wwlksnextbij  30262  clwlkclwwlklem2a1  30354  clwlkclwwlkf1  30372  eupth2eucrct  30579  frgrncvvdeq  30671  numclwlk2lem2fv  30740  numclwwlk2lem3  30742  ofoprabco  33020  fsuppcurry1  33080  fsuppcurry2  33081  offinsupp1  33082  ressprs  33295  mntoval  33311  mgcoval  33315  mndlactf1  33355  mndlactfo  33356  mndractf1  33357  mndractfo  33358  mndlactf1o  33359  mndractf1o  33360  lmodvslmhm  33379  gsummulsubdishift2  33398  gsumwrd2dccat  33407  cycpmco2f1  33453  cycpmco2rn  33454  cycpmco2lem2  33456  cycpmco2lem3  33457  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2  33462  conjga  33499  cntrval2  33500  fxpsubm  33501  fxpsubg  33502  fxpsubrg  33503  fxpsdrg  33504  archirngz  33518  archiabllem2a  33523  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnsubrunlem2  33577  rlocval  33588  fracval  33634  quslmod  33687  quslmhm  33688  quslvec  33689  unitprodclb  33711  nsgmgc  33730  nsgqusf1olem1  33731  nsgqusf1olem2  33732  nsgqusf1olem3  33733  lmhmqusker  33735  rhmquskerlem  33742  elrspunidl  33745  opprqusbas  33779  opprqusplusg  33780  opprqusmulr  33782  opprqus1r  33783  qsdrngilem  33785  qsdrngi  33786  rprmdvdsprod  33833  1arithidomlem1  33834  1arithidomlem2  33835  1arithidom  33836  1arithufdlem3  33845  dfufd2lem  33848  zringfrac  33853  evl1deg1  33875  evl1deg2  33876  evl1deg3  33877  ply1gsumz  33898  r1plmhm  33908  0mplrim  33913  selvply1rhmlema  33917  selvply1rhmlemb  33918  selvply1rhmlem1  33919  selvply1rhmlem3  33921  selvply1rhmlem4  33922  selvply1rhmlem5  33923  mplvrpmrhm  33946  psrgsum  33947  psrmonmul  33949  psrmonprod  33951  mplgsum  33952  splyval  33958  esplyfval1  33972  esplyfvaln  33973  vietadeg1  33977  resssra  33986  ply1degltdimlem  34021  ply1degltdim  34022  qusdimsum  34027  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  lactlmhm  34033  fldgenfldext  34067  evls1fldgencl  34069  fldextrspunlsplem  34072  fldextrspundgdvdslem  34079  fldextrspundgdvds  34080  extdgfialglem1  34091  extdgfialglem2  34092  extdgfialg  34093  algextdeglem4  34119  algextdeglem6  34121  algextdeglem7  34122  submateq  34208  lmatcl  34215  mdetpmtr1  34222  madjusmdetlem1  34226  madjusmdetlem3  34228  qqhvval  34382  esumfzf  34468  esumpfinvallem  34473  esumpmono  34478  esummulc1  34480  esumcvg  34485  esumgect  34489  ofcval  34498  omssubadd  34699  sitgfval  34740  sitmcl  34750  sseqfv2  34793  cndprobval  34832  ballotlemfval  34889  ballotlemsv  34909  ballotlemsf1o  34913  ofcccat  34942  signsplypnf  34946  signsply0  34947  signstfval  34960  signshf  34984  reprpmtf1o  35022  reprdifc  35023  logdivsqrle  35046  hgt750lemg  35050  hgt750lema  35053  lpadval  35075  cvmliftlem8  35792  cvmliftphtlem  35817  fmla1  35887  gonarlem  35894  sategoelfvb  35919  mrsubval  36009  ellcsrspsn  36141  r1peuqusdeg1  36143  fwddifval  36662  knoppcnlem1  37110  knoppcnlem6  37115  unbdqndv2lem2  37127  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem16  38315  poimirlem19  38318  poimirlem22  38321  poimirlem23  38322  broucube  38333  dvtan  38349  itg2addnc  38353  ibladdnc  38356  itgaddnc  38359  itgmulc2nclem2  38366  itgmulc2nc  38367  itgabsnc  38368  ftc1cnnclem  38370  ftc1anclem3  38374  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  dvasin  38383  dvacos  38384  dvreasin  38385  dvreacos  38386  areacirclem1  38387  areacirc  38392  fsumshftd  39754  hlrelat5N  40203  rhmzrhval  42767  aks6d1c1  42911  hashscontpow  42917  aks6d1c4  42919  aks6d1c2lem3  42921  aks6d1c2lem4  42922  aks6d1c2  42925  aks6d1c5lem0  42930  aks6d1c5lem3  42932  aks6d1c5lem2  42933  aks6d1c5  42934  sticksstones3  42943  sticksstones8  42948  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  aks6d1c6lem1  42965  aks6d1c6lem2  42966  aks6d1c6lem3  42967  aks6d1c6lem4  42968  aks6d1c6isolem1  42969  aks6d1c6isolem2  42970  aks6d1c6isolem3  42971  aks6d1c6lem5  42972  aks6d1c7lem2  42976  unitscyglem1  42990  readvrec2  43150  readvrec  43151  readvcot  43153  frlmfzolen  43305  frlmfzoccat  43307  frlmvscadiccat  43308  evlsbagval  43346  evlselv  43349  fsuppind  43350  mhpind  43354  mhphflem  43356  prjspner  43379  prjspnvs  43380  prjspnfv01  43384  prjspner01  43385  prjspner1  43386  0prjspnrel  43387  prjcrv0  43393  mzpclall  43486  mzpsubst  43507  eldioph2  43521  rabdiophlem2  43557  irrapxlem1  43577  mzpcong  43727  mendlmod  43944  naddcnff  44117  relexpmulnn  44463  iunrelexpuztr  44473  mnringvald  44965  mnringmulrvald  44979  radcnvrat  45052  hashnzfzclim  45060  lhe4.4ex1a  45067  expgrowthi  45071  expgrowth  45073  bccval  45076  binomcxplemrat  45088  binomcxplemfrat  45089  binomcxplemradcnv  45090  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  unirnmap  45952  unirnmapsn  45958  ssmapsn  45960  iocopn  46264  icoopn  46269  divcnvg  46371  sumnnodd  46374  climsubmpt  46402  dvsinax  46655  fperdvper  46661  dvdivf  46664  dvnprodlem1  46688  itgsincmulx  46716  stoweidlem59  46801  etransclem4  46980  etransclem13  46989  etransclem25  47001  etransclem48  47024  rrxtopnfi  47029  sge0tsms  47122  elhoi  47284  ovnval2  47287  ovnval2b  47294  ovncvrrp  47306  ovn0lem  47307  ovncl  47309  ovnome  47315  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvle  47342  ovnlecvr2  47352  ovncvr2  47353  ovnsubadd2lem  47387  ovnovollem1  47398  vonvolmbl  47403  iunhoiioolem  47417  vonioolem1  47422  vonioolem2  47423  vonicclem2  47426  smfresal  47530  smfres  47532  smfmullem4  47536  smfco  47544  adddmmbl  47575  muldmmbl  47577  chnsuslle  47625  sinnpoly  47656  fmtno  48309  isubgruhgr  48661  grtriprop  48734  grtriclwlk3  48738  gpgvtx  48836  gpgiedg  48837  intopval  48995  clintopval  48997  rngchomALTV  49061  funcringcsetcALTV2lem5  49087  ringchomALTV  49095  funcringcsetclem5ALTV  49110  srhmsubcALTVlem2  49117  srhmsubcALTV  49118  fldhmsubcALTV  49126  zlmodzxzscm  49165  zlmodzxzadd  49166  rmsupp0  49176  domnmsuppn0  49177  rmsuppss  49178  ply1mulgsumlem3  49196  ply1mulgsumlem4  49197  ply1mulgsum  49198  dmatALTval  49208  lincop  49216  lincval  49217  linc1  49233  lincresunit3lem1  49287  fdivmpt  49348  fdivmptfv  49353  refdivmptfv  49354  digval  49406  2arymptfv  49458  2arymaptfo  49462  itcovalpclem1  49478  itcovalt2lem1  49483  ackvalsuc1mpt  49486  ackval1  49489  ackval2  49490  ackval3  49491  ackval42  49504  line2xlem  49561  upfval2  49983  swapfval  50068  tposcurf1  50105  tposcurf2val  50107  fucofvalg  50124  fuco112x  50138  fuco23  50147  fucoid  50154  fucocolem4  50162  prcofvalg  50182  prcof1  50194  opf2fval  50211  lanval  50425  ranval  50426  crosspdot0i  50672