Theorem ovexd 6944

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

Syntax hints:   → wi 4   ∈ wcel 2164  Vcvv 3414  (class class class)co 6910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-nul 5015

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-sn 4400  df-pr 4402  df-uni 4661  df-iota 6090  df-fv 6135  df-ov 6913

This theorem is referenced by:  caofass  7196  caofdi  7198  caofdir  7199  caonncan  7200  mapsnend  8307  snmapen  8309  pw2eng  8341  mapen  8399  mapxpen  8401  mapdom2  8406  cantnfcl  8848  cantnflem1  8870  cnfcomlem  8880  cnfcom3lem  8884  cda1dif  9320  fzen  12658  seqf1o  13143  wrdnval  13612  pfxval  13759  pfxswrd  13793  splvalpfxOLD  13866  splval  13867  splvalOLD  13868  cshwsexa  13952  ofccat  14094  climshftlem  14689  climshft  14691  climshft2  14697  caucvgr  14790  fsumrev  14892  hashdvds  15858  setsabs  16272  ressress  16309  prdsvscafval  16500  qusval  16562  xpsbas  16594  xpsadd  16596  xpsmul  16597  xpssca  16598  xpsvsca  16599  xpsless  16600  xpsle  16601  homfval  16711  comfval  16719  cicfval  16816  rescabs  16852  rescabs2  16853  resscat  16871  fucbas  16979  fuccoval  16982  setchom  17089  catchom  17108  catcco  17110  estrchom  17126  funcestrcsetclem5  17144  funcsetcestrclem5  17159  evlf2val  17219  curf11  17226  curf12  17227  curf2val  17230  uncfval  17234  diagval  17240  hof2  17257  yonval  17261  gsumval2a  17639  gsumval2  17640  gsumwspan  17744  orbstafun  18101  orbstaval  18102  psgnvalii  18287  lsmhash  18476  frgpupval  18547  qusabl  18628  gsumval3  18668  gsumzaddlem  18681  gsummptshft  18696  telgsumfzslem  18746  telgsumfz  18748  telgsumfz0  18750  dpjval  18816  srgbinomlem3  18903  srgbinomlem4  18904  mulgass3  18998  lcomfsupp  19266  rmodislmodlem  19293  rmodislmod  19294  sraval  19544  srasca  19549  crngridl  19606  quscrng  19608  gsumbagdiaglem  19743  psrass1lem  19745  psrass1  19773  psrdi  19774  psrdir  19775  psrass23l  19776  mplval  19796  mplsubglem  19802  mplsubrglem  19807  mplmonmul  19832  mplcoe1  19833  opsrval  19842  psrbagev1  19877  evlslem6  19880  evlslem1  19882  evlsval  19886  mpfconst  19897  mpff  19900  mpfaddcl  19901  mpfmulcl  19902  mpfind  19903  ply1lss  19933  gsumply1subr  19971  coe1add  20001  coe1tm  20010  coe1tmmul  20014  cply1mul  20031  ply1coe  20033  evl1expd  20076  pf1mpf  20083  pf1ind  20086  znval  20250  znzrhfo  20262  znunithash  20279  cygznlem2  20283  pjfval  20420  pjpm  20422  frlmgsum  20485  frlmipval  20492  frlmphllem  20493  frlmphl  20494  frlmsslsp  20509  mamufv  20567  mamuass  20582  mamuvs1  20585  mamuvs2  20586  matgsum  20617  dmatmul  20678  scmatval  20685  scmatrhmval  20708  mvmulfv  20725  mavmulfv  20727  mavmulass  20730  marrepeval  20744  marepveval  20749  submaeval  20763  mdetrsca  20784  mdetunilem9  20801  mdetuni0  20802  gsummatr01lem3  20839  gsummatr01lem4  20840  gsummatr01  20841  smadiadetlem3  20850  cramerlem1  20870  mat2pmatmul  20913  m2cpminvid  20935  decpmatfsupp  20951  decpmatmullem  20953  decpmatmul  20954  decpmatmulsumfsupp  20955  pmatcollpw1lem1  20956  pmatcollpw3fi1lem1  20968  pmatcollpwscmatlem2  20972  pm2mpfval  20978  pm2mpf  20980  mply1topmatcllem  20985  mp2pm2mplem3  20990  mp2pm2mplem4  20991  pm2mpmhmlem1  21000  pm2mpmhmlem2  21001  pm2mp  21007  chfacfscmulfsupp  21041  chfacfscmulgsum  21042  chfacfpmmulfsupp  21045  chfacfpmmulgsum  21046  cpmidpmatlem3  21054  cpmadugsumlemB  21056  cpmadugsumlemC  21057  cpmadugsumlemF  21058  cayhamlem4  21070  xpstopnlem2  21992  fcfval  22214  tsmsxplem1  22333  tsmsxplem2  22334  tusval  22447  xpsdsfn  22559  xpsxmet  22562  xpsdsval  22563  xpsmet  22564  tmsval  22663  met1stc  22703  metuval  22731  cnmpt2pc  23104  pi1val  23213  pi1addf  23223  pi1addval  23224  pi1grplem  23225  rrxnm  23566  rrxcph  23567  rrxmval  23580  mbfmulc2  23836  mbfmul  23899  itg2mulclem  23919  ibladd  23993  itgadd  23997  itgabs  24007  bddmulibl  24011  dvmulf  24112  dvcmulf  24114  dvmptmul  24130  dvlip  24162  ftc1lem4  24208  mdegmullem  24244  coe1mul3  24265  r1pval  24322  plyco  24403  dgrcolem1  24435  elqaalem3  24482  taylpfval  24525  taylthlem2  24534  pserdvlem2  24588  advlogexp  24807  logtayl  24812  logccv  24815  dvcxp1  24890  dvcncxp1  24893  logbmpt  24935  logbfval  24937  relogbf  24938  dvatan  25082  cxp2lim  25123  cxploglim2  25125  lgamgulmlem2  25176  lgamgulm2  25182  lgamcvglem  25186  lgamf  25188  basellem7  25233  basellem8  25234  basellem9  25235  fsumdvdscom  25331  logexprlim  25370  dchrfi  25400  gausslemma2dlem2  25512  gausslemma2dlem3  25513  2lgslem1b  25537  chtppilimlem2  25583  chebbnd2  25586  chto1lb  25587  chpchtlim  25588  chpo1ub  25589  vmadivsum  25591  dchrisum0lem3  25628  mudivsum  25639  logdivsum  25642  log2sumbnd  25653  selberglem1  25654  selberg2lem  25659  selberg2  25660  selbergr  25677  wlkp1  26989  wwlksnextsurj  27221  wwlksnextsurOLD  27226  wwlksnextbij  27228  wwlksnextbijOLD  27229  clwlkclwwlklem2a1  27328  clwlkclwwlkf1OLD  27350  clwlkclwwlkf1  27354  eupth2eucrct  27590  frgrncvvdeq  27686  numclwlk2lem2fv  27777  numclwlk2lem2fvOLD  27780  numclwwlk2lem3  27782  numclwwlk2lem3OLD  27783  numclwlk2lem2fvOLDOLD  27788  numclwwlk2lem3OLDOLD  27790  ofoprabco  30009  ressprs  30196  resspos  30200  archirngz  30284  archiabllem2a  30289  submateq  30416  lmatcl  30423  mdetpmtr1  30430  madjusmdetlem1  30434  madjusmdetlem3  30436  qqhvval  30568  esumfzf  30672  esumpfinvallem  30677  esumpmono  30682  esummulc1  30684  esumcvg  30689  esumgect  30693  ofcval  30702  omssubadd  30903  sitgfval  30944  sitmcl  30954  sseqfv2  30998  cndprobval  31037  ballotlemfval  31093  ballotlemsv  31113  ballotlemsf1o  31117  ofcccat  31163  signsplypnf  31170  signsply0  31171  signstfval  31184  signshf  31210  reprpmtf1o  31249  reprdifc  31250  logdivsqrle  31273  hgt750lemg  31277  hgt750lema  31280  cvmliftlem8  31816  cvmliftphtlem  31841  mrsubval  31948  fwddifval  32803  knoppcnlem1  33011  knoppcnlem6  33016  unbdqndv2lem2  33028  poimirlem1  33953  poimirlem2  33954  poimirlem3  33955  poimirlem5  33957  poimirlem6  33958  poimirlem7  33959  poimirlem10  33962  poimirlem11  33963  poimirlem12  33964  poimirlem16  33968  poimirlem19  33971  poimirlem22  33974  poimirlem23  33975  broucube  33986  dvtan  34002  itg2addnc  34006  ibladdnc  34009  itgaddnc  34012  itgmulc2nclem2  34019  itgmulc2nc  34020  itgabsnc  34021  ftc1cnnclem  34025  ftc1anclem3  34029  ftc1anclem6  34032  ftc1anclem7  34033  ftc1anclem8  34034  dvasin  34038  dvacos  34039  dvreasin  34040  dvreacos  34041  areacirclem1  34042  areacirc  34047  fsumshftd  35026  hlrelat5N  35475  mzpclall  38133  mzpsubst  38154  eldioph2  38168  rabdiophlem2  38209  irrapxlem1  38229  mzpcong  38381  mendlmod  38605  relexpmulnn  38841  iunrelexpuztr  38851  radcnvrat  39352  hashnzfzclim  39360  lhe4.4ex1a  39367  expgrowthi  39371  expgrowth  39373  bccval  39376  binomcxplemrat  39388  binomcxplemfrat  39389  binomcxplemradcnv  39390  binomcxplemdvbinom  39391  binomcxplemdvsum  39393  binomcxplemnotnn0  39394  unirnmap  40205  unirnmapsn  40211  ssmapsn  40213  iocopn  40540  icoopn  40545  divcnvg  40652  sumnnodd  40655  climsubmpt  40685  dvsinax  40920  fperdvper  40926  dvdivf  40930  dvnprodlem1  40954  itgsincmulx  40982  stoweidlem59  41068  etransclem4  41247  etransclem13  41256  etransclem25  41268  etransclem48  41291  rrxtopnfi  41296  sge0tsms  41386  elhoi  41548  ovnval2  41551  ovnval2b  41558  ovncvrrp  41570  ovn0lem  41571  ovncl  41573  ovnome  41579  hoidmvlelem2  41602  hoidmvlelem3  41603  hoidmvle  41606  ovnlecvr2  41616  ovncvr2  41617  ovnsubadd2lem  41651  ovnovollem1  41662  vonvolmbl  41667  iunhoiioolem  41681  vonioolem1  41686  vonioolem2  41687  vonicclem2  41690  smfresal  41787  smfres  41789  smfmullem4  41793  smfco  41801  fmtno  42289  intopval  42703  clintopval  42705  rngcval  42827  rnghmsscmap2  42838  rnghmsscmap  42839  rngchomALTV  42850  funcrngcsetc  42863  ringcval  42873  rhmsscmap2  42884  rhmsscmap  42885  funcringcsetc  42900  funcringcsetcALTV2lem5  42905  ringchomALTV  42913  funcringcsetclem5ALTV  42928  srhmsubclem3  42940  srhmsubc  42941  fldhmsubc  42949  srhmsubcALTVlem2  42958  srhmsubcALTV  42959  fldhmsubcALTV  42967  zlmodzxzscm  43000  zlmodzxzadd  43001  rmsupp0  43014  domnmsuppn0  43015  rmsuppss  43016  ply1mulgsumlem3  43041  ply1mulgsumlem4  43042  ply1mulgsum  43043  dmatALTval  43054  lincop  43062  lincval  43063  linc1  43079  lincresunit3lem1  43133  fdivmpt  43199  fdivmptfv  43204  refdivmptfv  43205  digval  43257  line2xlem  43319