MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unieqd Unicode version

Theorem unieqd 4259
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1
Assertion
Ref Expression
unieqd

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2
2 unieq 4257 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  U.cuni 4249
This theorem is referenced by:  uniprg  4263  unisng  4265  unisn3  4266  csbuni  4277  unisn2  4588  opswap  5500  unixpid  5547  iotaeq  5564  iotabi  5565  uniabio  5566  iotanul  5571  funfv  5940  funfv2  5941  fvun  5943  dffv2  5946  fniunfv  6159  ordunisuc  6667  orduniss2  6668  onsucuni2  6669  elxp4  6744  elxp5  6745  1stval  6802  2ndval  6803  1stnpr  6804  2ndnpr  6805  fo1st  6820  fo2nd  6821  f1stres  6822  f2ndres  6823  1st2val  6826  2nd2val  6827  2nd1st  6845  cnvf1olem  6898  brtpos2  6980  dftpos4  6993  tpostpos  6994  recseq  7062  tz7.44-2  7092  tz7.44-3  7093  rdglim2  7117  ixpsnf1o  7529  xpcomco  7627  xpassen  7631  xpdom2  7632  supeq1  7925  supeq2  7928  supeq3  7929  supeq123d  7930  supval2  7935  rankuni  8302  en2other2  8408  dfac2a  8531  dfac12lem1  8544  dfac12r  8547  kmlem9  8559  kmlem11  8561  kmlem12  8562  enfin2i  8722  fin23lem29  8742  fin23lem30  8743  fin23lem32  8745  fin23lem34  8747  fin23lem35  8748  fin23lem36  8749  fin23lem38  8750  fin23lem39  8751  fin23lem41  8753  isf34lem7  8780  isf34lem6  8781  fin1a2lem10  8810  fin1a2lem11  8811  fin1a2lem12  8812  itunisuc  8820  itunitc  8822  ttukeylem3  8912  ttukey2g  8917  pwcfsdom  8979  gruurn  9197  dfinfmr  10545  fsumcnv  13588  fprodcnv  13787  xpnnenOLD  13943  mrcun  15019  isacs1i  15054  mreacs  15055  arwval  15370  ipoval  15784  isacs5lem  15799  acsdrscl  15800  acsficl  15801  isps  15832  isdir  15862  pmtrval  16476  pmtrfv  16477  pmtrprfv  16478  pmtrdifellem3  16503  pmtrprfval  16512  gsumcom2  17003  dmdprd  17029  dprddisj  17042  dprdf1o  17079  dprdsn  17083  dprd2da  17091  dprd2db  17092  dmdprdsplit2lem  17094  lspuni0  17656  lss0v  17662  zrhval  18545  zrhval2  18546  zrhpropd  18552  isbasisg  19448  basis1  19451  baspartn  19455  tgval  19456  eltg  19458  ntrfval  19525  ntrval  19537  tgrest  19660  restuni2  19668  lmfval  19733  cnfval  19734  cnpfval  19735  pnrmopn  19844  fiuncmp  19904  cmpfi  19908  ptval  20071  ptpjpre1  20072  elptr2  20075  ptuni2  20077  ptbasin  20078  ptbasfi  20082  xkoval  20088  txtopon  20092  ptuni  20095  ptunimpt  20096  xkouni  20100  ptpjcn  20112  ptcld  20114  dfac14  20119  ptcnp  20123  prdstopn  20129  ptrescn  20140  txcmplem2  20143  xkoptsub  20155  xkopt  20156  qtopval  20196  qtopeu  20217  hmphindis  20298  txswaphmeolem  20305  ptuncnv  20308  ptunhmeo  20309  xpstopnlem1  20310  flimval  20464  fcfval  20534  alexsubALTlem3  20549  ptcmplem1  20552  ptcmplem2  20553  ptcmplem3  20554  ptcmplem4  20555  ptcmpg  20557  cnextfres  20568  cldsubg  20609  utopval  20735  tusval  20769  tuslem  20770  tususs  20773  ucnval  20780  prdsxmslem2  21032  ishtpy  21472  pi1buni  21540  pi1xfrcnv  21557  elovolmr  21887  ovoliunlem3  21915  uniioombllem2  21992  uniioombllem3  21994  dyadmbl  22009  vmaval  23387  vmappw  23390  disjabrex  27443  disjabrexf  27444  fcnvgreu  27514  xrge0tsmseq  27777  locfinreflem  27843  locfinref  27844  pstmval  27874  pstmfval  27875  ordtprsuni  27901  esumeq12dvaf  28044  esumeq2  28049  esumval  28057  esumf1o  28061  esumsn  28072  esumss  28078  esumpfinval  28081  esumpfinvalf  28082  sxsigon  28163  meascnbl  28190  brae  28213  braew  28214  faeval  28218  imambfm  28233  cnmbfm  28234  dya2iocuni  28254  omsval  28264  omsfval  28265  oms0  28266  omsmon  28267  elprob  28348  probfinmeasb  28368  probmeasb  28369  dstrvprob  28410  indispcon  28679  iscvm  28704  cvmscld  28718  msrfval  28897  msrval  28898  mthmpps  28942  relexp0  29052  relexpsucr  29053  rdgprc0  29226  rdgprc  29227  dfrdg2  29228  dfrdg3  29229  trpredeq1  29303  trpredeq2  29304  trpredeq3  29305  wrecseq123  29337  nofulllem1  29462  nofulllem2  29463  unisnif  29575  brapply  29588  ordcmp  29912  ptrest  30048  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  isfne  30157  fnemeet2  30185  fnejoin2  30187  tailfval  30190  aomclem8  31007  dfac21  31012  stoweidlem39  31821  csbfv12gALTOLD  33621  mapdunirnN  37377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250
  Copyright terms: Public domain W3C validator