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

Theorem unieqd 4218
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 4216 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  U.cuni 4208
This theorem is referenced by:  uniprg  4222  unisng  4224  unisn3  4225  csbuni  4236  unisn2  4545  opswap  5445  unixpid  5491  iotaeq  5508  iotabi  5509  uniabio  5510  iotanul  5515  funfv  5881  funfv2  5882  fvun  5884  dffv2  5887  fniunfv  6089  ordunisuc  6576  orduniss2  6577  onsucuni2  6578  elxp4  6655  elxp5  6656  1stval  6712  2ndval  6713  1stnpr  6714  2ndnpr  6715  fo1st  6729  fo2nd  6730  f1stres  6731  f2ndres  6732  1st2val  6735  2nd2val  6736  2nd1st  6752  cnvf1olem  6804  brtpos2  6885  dftpos4  6898  tpostpos  6899  recseq  6967  tz7.44-2  6997  tz7.44-3  6998  rdglim2  7022  ixpsnf1o  7437  xpcomco  7535  xpassen  7539  xpdom2  7540  supeq1  7831  supeq2  7834  supeq3  7835  supeq123d  7836  supval2  7841  rankuni  8207  en2other2  8313  dfac2a  8436  dfac12lem1  8449  dfac12r  8452  kmlem9  8464  kmlem11  8466  kmlem12  8467  enfin2i  8627  fin23lem29  8647  fin23lem30  8648  fin23lem32  8650  fin23lem34  8652  fin23lem35  8653  fin23lem36  8654  fin23lem38  8655  fin23lem39  8656  fin23lem41  8658  isf34lem7  8685  isf34lem6  8686  fin1a2lem10  8715  fin1a2lem11  8716  fin1a2lem12  8717  itunisuc  8725  itunitc  8727  ttukeylem3  8817  ttukey2g  8822  pwcfsdom  8884  gruurn  9102  dfinfmr  10444  fsumcnv  13398  xpnnenOLD  13650  mrcun  14719  isacs1i  14754  mreacs  14755  arwval  15070  ipoval  15483  isacs5lem  15498  acsdrscl  15499  acsficl  15500  isps  15531  isdir  15561  pmtrval  16116  pmtrfv  16117  pmtrprfv  16118  pmtrdifellem3  16143  pmtrprfval  16152  gsumcom2  16636  dmdprd  16655  dprddisj  16668  dprdf1o  16704  dprdsn  16708  dprd2da  16716  dprd2db  16717  dmdprdsplit2lem  16719  lspuni0  17267  lss0v  17273  zrhval  18132  zrhval2  18133  zrhpropd  18139  isbasisg  18951  basis1  18954  baspartn  18958  tgval  18959  eltg  18961  ntrfval  19027  ntrval  19039  tgrest  19162  restuni2  19170  lmfval  19235  cnfval  19236  cnpfval  19237  pnrmopn  19346  fiuncmp  19406  cmpfi  19410  ptval  19542  ptpjpre1  19543  elptr2  19546  ptuni2  19548  ptbasin  19549  ptbasfi  19553  xkoval  19559  txtopon  19563  ptuni  19566  ptunimpt  19567  xkouni  19571  ptpjcn  19583  ptcld  19585  dfac14  19590  ptcnp  19594  prdstopn  19600  ptrescn  19611  txcmplem2  19614  xkoptsub  19626  xkopt  19627  qtopval  19667  qtopeu  19688  hmphindis  19769  txswaphmeolem  19776  ptuncnv  19779  ptunhmeo  19780  xpstopnlem1  19781  flimval  19935  fcfval  20005  alexsubALTlem3  20020  ptcmplem1  20023  ptcmplem2  20024  ptcmplem3  20025  ptcmplem4  20026  ptcmpg  20028  cnextfres  20039  cldsubg  20080  utopval  20206  tusval  20240  tuslem  20241  tususs  20244  ucnval  20251  prdsxmslem2  20503  ishtpy  20943  pi1buni  21011  pi1xfrcnv  21028  cmetcusp  21265  elovolmr  21358  ovoliunlem3  21386  uniioombllem2  21463  uniioombllem3  21465  dyadmbl  21480  vmaval  22851  vmappw  22854  disjabrex  26394  disjabrexf  26395  fcnvgreu  26458  xrge0tsmseq  26712  pstmval  26779  pstmfval  26780  ordtprsuni  26806  esumeq12dvaf  26944  esumeq2  26949  esumval  26957  esumf1o  26961  esumsn  26972  esumss  26978  esumpfinval  26981  esumpfinvalf  26982  sxsigon  27063  meascnbl  27090  brae  27113  braew  27114  faeval  27118  imambfm  27133  cnmbfm  27134  dya2iocuni  27154  omsval  27164  omsfval  27165  oms0  27166  omsmon  27167  elprob  27248  probfinmeasb  27268  probmeasb  27269  dstrvprob  27310  indispcon  27579  iscvm  27604  cvmscld  27618  relexp0  27787  relexpsucr  27788  fprodcnv  27950  rdgprc0  28063  rdgprc  28064  dfrdg2  28065  dfrdg3  28066  trpredeq1  28140  trpredeq2  28141  trpredeq3  28142  wrecseq123  28174  nofulllem1  28299  nofulllem2  28300  unisnif  28412  brapply  28425  ordcmp  28749  ptrest  28885  mblfinlem2  28889  ovoliunnfl  28893  voliunnfl  28895  volsupnfl  28896  isfne  29000  fnemeet2  29048  fnejoin2  29050  tailfval  29053  aomclem8  29874  dfac21  29879  stoweidlem39  30568  csbfv12gALTOLD  32400  mapdunirnN  36146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2806  df-uni 4209
  Copyright terms: Public domain W3C validator