Theorem ovexd 7465

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-sn 4631  df-pr 4633  df-uni 4912  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  caofass  7735  caofdi  7737  caofdir  7738  caonncan  7739  suppofssd  8226  mapsnend  9074  snmapen  9076  pw2eng  9116  mapen  9179  mapxpen  9181  mapunen  9184  mapdom2  9186  cantnfcl  9704  cantnfle  9708  cantnflt  9709  cantnflt2  9710  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1d  9725  cantnflem1  9726  cnfcomlem  9736  cnfcom  9737  cnfcom2lem  9738  cnfcom3lem  9740  fzen  13577  seqf1o  14080  wrdexg  14558  wrdnval  14579  pfxval  14707  pfxswrd  14740  splval  14785  cshwsexaOLD  14859  ofccat  15004  climshftlem  15606  climshft  15608  climshft2  15614  caucvgr  15708  fsumrev  15811  hashdvds  16808  setsabs  17212  ressress  17293  firest  17478  prdsvscafval  17526  qusval  17588  xpsbas  17618  xpsadd  17620  xpsmul  17621  xpssca  17622  xpsvsca  17623  xpsless  17624  xpsle  17625  homfval  17736  comfval  17744  cicfval  17844  rescabs  17882  rescabsOLD  17883  rescabs2  17884  resscat  17902  funcres2c  17954  ressffth  17991  fucbas  18015  fuccoval  18019  setchom  18133  catchom  18156  catcco  18158  estrchom  18181  funcestrcsetclem5  18199  funcsetcestrclem5  18214  evlf2val  18275  curf11  18282  curf12  18283  curf2val  18286  uncfval  18290  diagval  18296  hof2  18313  yonval  18317  gsumval2a  18710  gsumval2  18711  mndpsuppss  18790  gsumwspan  18871  efmnd  18895  ghmqusnsglem1  19310  ghmqusnsglem2  19311  ghmqusnsg  19312  ghmquskerlem1  19313  ghmquskerco  19314  ghmquskerlem2  19315  ghmquskerlem3  19316  ghmqusker  19317  orbstafun  19341  orbstaval  19342  symgval  19402  psgnvalii  19541  lsmhash  19737  frgpupval  19806  qusabl  19897  gsumval3  19939  gsumreidx  19949  gsumzaddlem  19953  gsummptshft  19968  telgsumfzslem  20020  telgsumfz  20022  telgsumfz0  20024  dpjval  20090  prdsrngd  20193  srgbinomlem3  20245  srgbinomlem4  20246  mulgass3  20369  rngcval  20634  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  ringcval  20663  rhmsscmap2  20674  rhmsscmap  20675  funcringcsetc  20690  srhmsubclem3  20695  srhmsubc  20696  fldhmsubc  20802  lcomfsupp  20916  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  sraval  21191  srasca  21200  srascaOLD  21201  crngridl  21307  quscrng  21310  rhmqusnsg  21312  pzriprnglem11  21519  znval  21567  znzrhfo  21583  znunithash  21600  cygznlem2  21604  frobrhm  21611  pjfval  21743  pjpm  21745  frlmgsum  21809  frlmipval  21816  frlmphllem  21817  frlmphl  21818  frlmsslsp  21833  frlmup1  21835  gsumbagdiaglem  21967  psrass1lem  21969  rhmpsrlem1  21977  psrass1  22001  psrdi  22002  psrdir  22003  psrass23l  22004  psrascl  22016  mplval  22026  mplsubglem  22036  mplsubrglem  22041  mplmonmul  22071  mplcoe1  22072  opsrval  22081  psrbagev1  22118  psrbagev2  22119  evlslem6  22122  evlslem1  22123  evlsval  22127  mpfconst  22142  mpff  22145  mpfaddcl  22146  mpfmulcl  22147  mpfind  22148  mhpmulcl  22170  mhpaddcl  22172  psdcoef  22181  psdmplcl  22183  psdadd  22184  ply1lss  22213  gsumply1subr  22250  coe1add  22282  coe1tm  22291  coe1tmmul  22295  cply1mul  22315  ply1coe  22317  evl1expd  22364  pf1mpf  22371  pf1ind  22374  mhmcompl  22399  mhmcoaddmpl  22400  rhmmpl  22402  rhmply1vsca  22407  mamufv  22413  mamuass  22421  mamuvs1  22424  mamuvs2  22425  matgsum  22458  dmatmul  22518  scmatval  22525  scmatrhmval  22548  mvmulfv  22565  mavmulfv  22567  mavmulass  22570  marrepeval  22584  marepveval  22589  submaeval  22603  mdetrsca  22624  mdetunilem9  22641  mdetuni0  22642  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  smadiadetlem3  22689  cramerlem1  22708  mat2pmatmul  22752  m2cpminvid  22774  decpmatfsupp  22790  decpmatmullem  22792  decpmatmul  22793  decpmatmulsumfsupp  22794  pmatcollpw1lem1  22795  pmatcollpw3fi1lem1  22807  pmatcollpwscmatlem2  22811  pm2mpfval  22817  pm2mpf  22819  mply1topmatcllem  22824  mp2pm2mplem3  22829  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  pm2mpmhmlem2  22840  pm2mp  22846  chfacfscmulfsupp  22880  chfacfscmulgsum  22881  chfacfpmmulfsupp  22884  chfacfpmmulgsum  22885  cpmidpmatlem3  22893  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  cayhamlem4  22909  xpstopnlem2  23834  fcfval  24056  tsmsxplem1  24176  tsmsxplem2  24177  tusval  24289  xpsdsfn  24402  xpsxmet  24405  xpsdsval  24406  xpsmet  24407  tmsval  24508  met1stc  24549  metuval  24577  cnmpopc  24968  pi1val  25083  pi1addf  25093  pi1addval  25094  pi1grplem  25095  rrxnm  25438  rrxcph  25439  rrxmval  25452  mbfmulc2  25711  mbfmul  25775  itg2mulclem  25795  ibladd  25870  itgadd  25874  itgabs  25884  bddmulibl  25888  dvmulf  25994  dvcmulf  25996  dvmptmul  26013  cmvth  26043  dvlip  26046  ftc1lem4  26094  mdegmullem  26131  coe1mul3  26152  r1pval  26211  plyco  26294  dgrcolem1  26327  elqaalem3  26377  taylpfval  26420  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  advlogexp  26711  logtayl  26716  logccv  26719  dvcxp1  26796  dvcncxp1  26799  logbmpt  26845  logbfval  26847  relogbf  26848  dvatan  26992  cxp2lim  27034  cxploglim2  27036  lgamgulmlem2  27087  lgamgulm2  27093  lgamcvglem  27097  lgamf  27099  basellem7  27144  basellem8  27145  basellem9  27146  fsumdvdscom  27242  logexprlim  27283  dchrfi  27313  gausslemma2dlem2  27425  gausslemma2dlem3  27426  2lgslem1b  27450  chtppilimlem2  27532  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  vmadivsum  27540  dchrisum0lem3  27577  mudivsum  27588  logdivsum  27591  log2sumbnd  27602  selberglem1  27603  selberg2lem  27608  selberg2  27609  selbergr  27626  negsval  28071  wlkp1  29713  wwlksnextsurj  29929  wwlksnextbij  29931  clwlkclwwlklem2a1  30020  clwlkclwwlkf1  30038  eupth2eucrct  30245  frgrncvvdeq  30337  numclwlk2lem2fv  30406  numclwwlk2lem3  30408  ofoprabco  32680  fsuppcurry1  32742  fsuppcurry2  32743  offinsupp1  32744  ressprs  32938  resspos  32940  mntoval  32956  mgcoval  32960  mndlactf1  33013  mndlactfo  33014  mndractf1  33015  mndractfo  33016  mndlactf1o  33017  mndractf1o  33018  lmodvslmhm  33035  gsumwrd2dccat  33052  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  archirngz  33178  archiabllem2a  33183  elrgspnlem1  33231  elrgspnlem2  33232  rlocval  33245  fracval  33285  quslmod  33365  quslmhm  33366  quslvec  33367  qustriv  33371  qustrivr  33372  unitprodclb  33396  nsgmgc  33419  nsgqusf1olem1  33420  nsgqusf1olem2  33421  nsgqusf1olem3  33422  lmhmqusker  33424  rhmquskerlem  33432  elrspunidl  33435  qsidomlem1  33459  qsidomlem2  33460  opprqusbas  33495  opprqusplusg  33496  opprqusmulr  33498  opprqus1r  33499  qsdrngilem  33501  qsdrngi  33502  rprmdvdsprod  33541  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  1arithufdlem3  33553  dfufd2lem  33556  zringfrac  33561  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  ply1gsumz  33598  r1plmhm  33609  resssra  33616  ply1degltdimlem  33649  ply1degltdim  33650  qusdimsum  33655  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  lactlmhm  33661  fldgenfldext  33692  evls1fldgencl  33694  algextdeglem4  33725  algextdeglem6  33727  algextdeglem7  33728  submateq  33769  lmatcl  33776  mdetpmtr1  33783  madjusmdetlem1  33787  madjusmdetlem3  33789  qqhvval  33945  esumfzf  34049  esumpfinvallem  34054  esumpmono  34059  esummulc1  34061  esumcvg  34066  esumgect  34070  ofcval  34079  omssubadd  34281  sitgfval  34322  sitmcl  34332  sseqfv2  34375  cndprobval  34414  ballotlemfval  34470  ballotlemsv  34490  ballotlemsf1o  34494  ofcccat  34536  signsplypnf  34543  signsply0  34544  signstfval  34557  signshf  34581  reprpmtf1o  34619  reprdifc  34620  logdivsqrle  34643  hgt750lemg  34647  hgt750lema  34650  lpadval  34669  cvmliftlem8  35276  cvmliftphtlem  35301  fmla1  35371  gonarlem  35378  sategoelfvb  35403  mrsubval  35493  ellcsrspsn  35625  r1peuqusdeg1  35627  fwddifval  36143  knoppcnlem1  36475  knoppcnlem6  36480  unbdqndv2lem2  36492  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem19  37625  poimirlem22  37628  poimirlem23  37629  broucube  37640  dvtan  37656  itg2addnc  37660  ibladdnc  37663  itgaddnc  37666  itgmulc2nclem2  37673  itgmulc2nc  37674  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem3  37681  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  dvasin  37690  dvacos  37691  dvreasin  37692  dvreacos  37693  areacirclem1  37694  areacirc  37699  fsumshftd  38933  hlrelat5N  39383  rhmzrhval  41951  aks6d1c1  42097  hashscontpow  42103  aks6d1c4  42105  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks6d1c5  42120  sticksstones3  42129  sticksstones8  42134  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks6d1c7lem2  42162  unitscyglem1  42176  readvrec2  42369  readvrec  42370  frlmfzolen  42489  frlmfzoccat  42491  frlmvscadiccat  42492  evlscl  42544  evlsval3  42545  evlsvval  42546  evlsvvval  42549  evlsbagval  42552  evlsexpval  42553  evlsaddval  42554  evlsmulval  42555  evlsevl  42557  evlcl  42558  evladdval  42561  evlmulval  42562  selvcl  42569  evlselv  42573  fsuppind  42576  mhpind  42580  mhphflem  42582  prjspner  42605  prjspnvs  42606  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  0prjspnrel  42613  prjcrv0  42619  mzpclall  42714  mzpsubst  42735  eldioph2  42749  rabdiophlem2  42789  irrapxlem1  42809  mzpcong  42960  mendlmod  43177  naddcnff  43351  relexpmulnn  43698  iunrelexpuztr  43708  mnringvald  44203  mnringmulrvald  44222  radcnvrat  44309  hashnzfzclim  44317  lhe4.4ex1a  44324  expgrowthi  44328  expgrowth  44330  bccval  44333  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemradcnv  44347  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  unirnmap  45150  unirnmapsn  45156  ssmapsn  45158  iocopn  45472  icoopn  45477  divcnvg  45582  sumnnodd  45585  climsubmpt  45615  dvsinax  45868  fperdvper  45874  dvdivf  45877  dvnprodlem1  45901  itgsincmulx  45929  stoweidlem59  46014  etransclem4  46193  etransclem13  46202  etransclem25  46214  etransclem48  46237  rrxtopnfi  46242  sge0tsms  46335  elhoi  46497  ovnval2  46500  ovnval2b  46507  ovncvrrp  46519  ovn0lem  46520  ovncl  46522  ovnome  46528  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvle  46555  ovnlecvr2  46565  ovncvr2  46566  ovnsubadd2lem  46600  ovnovollem1  46611  vonvolmbl  46616  iunhoiioolem  46630  vonioolem1  46635  vonioolem2  46636  vonicclem2  46639  smfresal  46743  smfres  46745  smfmullem4  46749  smfco  46757  adddmmbl  46788  muldmmbl  46790  fmtno  47453  isubgruhgr  47791  grtriprop  47845  grtriclwlk3  47849  gpgvtx  47937  gpgiedg  47938  intopval  48045  clintopval  48047  rngchomALTV  48111  funcringcsetcALTV2lem5  48137  ringchomALTV  48145  funcringcsetclem5ALTV  48160  srhmsubcALTVlem2  48167  srhmsubcALTV  48168  fldhmsubcALTV  48176  zlmodzxzscm  48201  zlmodzxzadd  48202  rmsupp0  48212  domnmsuppn0  48213  rmsuppss  48214  ply1mulgsumlem3  48233  ply1mulgsumlem4  48234  ply1mulgsum  48235  dmatALTval  48245  lincop  48253  lincval  48254  linc1  48270  lincresunit3lem1  48324  fdivmpt  48389  fdivmptfv  48394  refdivmptfv  48395  digval  48447  2arymptfv  48499  2arymaptfo  48503  itcovalpclem1  48519  itcovalt2lem1  48524  ackvalsuc1mpt  48527  ackval1  48530  ackval2  48531  ackval3  48532  ackval42  48545  line2xlem  48602