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

Theorem unieqd 4076
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 4074 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  U.cuni 4066
This theorem is referenced by:  uniprg  4080  unisng  4082  unisn3  4083  csbuni  4094  unisn2  4403  opswap  5298  unixpid  5344  iotaeq  5361  iotabi  5362  uniabio  5363  iotanul  5368  funfv  5728  funfv2  5729  fvun  5731  dffv2  5734  fniunfv  5932  ordunisuc  6413  orduniss2  6414  onsucuni2  6415  elxp4  6492  elxp5  6493  1stval  6548  2ndval  6549  1stnpr  6550  2ndnpr  6551  fo1st  6565  fo2nd  6566  f1stres  6567  f2ndres  6568  1st2val  6571  2nd2val  6572  2nd1st  6588  cnvf1olem  6639  brtpos2  6713  dftpos4  6726  tpostpos  6727  recseq  6792  tz7.44-2  6822  tz7.44-3  6823  rdglim2  6847  ixpsnf1o  7262  xpcomco  7360  xpassen  7364  xpdom2  7365  supeq1  7642  supeq2  7645  supeq3  7646  supeq123d  7647  supval2  7652  rankuni  8017  en2other2  8123  dfac2a  8246  dfac12lem1  8259  dfac12r  8262  kmlem9  8274  kmlem11  8276  kmlem12  8277  enfin2i  8437  fin23lem29  8457  fin23lem30  8458  fin23lem32  8460  fin23lem34  8462  fin23lem35  8463  fin23lem36  8464  fin23lem38  8465  fin23lem39  8466  fin23lem41  8468  isf34lem7  8495  isf34lem6  8496  fin1a2lem10  8525  fin1a2lem11  8526  fin1a2lem12  8527  itunisuc  8535  itunitc  8537  ttukeylem3  8627  ttukey2g  8632  pwcfsdom  8694  gruurn  8911  dfinfmr  10253  fsumcnv  13181  xpnnenOLD  13432  mrcun  14500  isacs1i  14535  mreacs  14536  arwval  14851  ipoval  15264  isacs5lem  15279  acsdrscl  15280  acsficl  15281  isps  15312  isdir  15342  pmtrval  15894  pmtrfv  15895  pmtrprfv  15896  pmtrdifellem3  15921  pmtrprfval  15930  gsumcom2  16358  dmdprd  16368  dprddisj  16376  dprdf1o  16399  dprdsn  16403  dprd2da  16409  dprd2db  16410  dmdprdsplit2lem  16412  lspuni0  16900  lss0v  16906  zrhval  17647  zrhval2  17648  zrhpropd  17654  isbasisg  18256  basis1  18259  baspartn  18263  tgval  18264  eltg  18266  ntrfval  18332  ntrval  18344  tgrest  18467  restuni2  18475  lmfval  18540  cnfval  18541  cnpfval  18542  pnrmopn  18651  fiuncmp  18711  cmpfi  18715  ptval  18847  ptpjpre1  18848  elptr2  18851  ptuni2  18853  ptbasin  18854  ptbasfi  18858  xkoval  18864  txtopon  18868  ptuni  18871  ptunimpt  18872  xkouni  18876  ptpjcn  18888  ptcld  18890  dfac14  18895  ptcnp  18899  prdstopn  18905  ptrescn  18916  txcmplem2  18919  xkoptsub  18931  xkopt  18932  qtopval  18972  qtopeu  18993  hmphindis  19074  txswaphmeolem  19081  ptuncnv  19084  ptunhmeo  19085  xpstopnlem1  19086  flimval  19240  fcfval  19310  alexsubALTlem3  19325  ptcmplem1  19328  ptcmplem2  19329  ptcmplem3  19330  ptcmplem4  19331  ptcmpg  19333  cnextfres  19344  cldsubg  19385  utopval  19507  tusval  19541  tuslem  19542  tususs  19545  ucnval  19552  prdsxmslem2  19804  ishtpy  20244  pi1buni  20312  pi1xfrcnv  20329  cmetcusp  20566  elovolmr  20659  ovoliunlem3  20687  uniioombllem2  20763  uniioombllem3  20765  dyadmbl  20780  vmaval  22192  vmappw  22195  disjabrex  25606  disjabrexf  25607  fcnvgreu  25671  xrge0tsmseq  25963  pstmval  26031  pstmfval  26032  ordtprsuni  26058  esumeq12dvaf  26196  esumeq2  26201  esumval  26209  esumf1o  26213  esumsn  26224  esumss  26230  esumpfinval  26233  esumpfinvalf  26234  sxsigon  26315  meascnbl  26342  brae  26366  braew  26367  faeval  26371  imambfm  26386  cnmbfm  26387  dya2iocuni  26407  elprob  26495  probfinmeasb  26515  probmeasb  26516  dstrvprob  26557  indispcon  26826  iscvm  26851  cvmscld  26865  relexp0  27033  relexpsucr  27034  fprodcnv  27196  rdgprc0  27309  rdgprc  27310  dfrdg2  27311  dfrdg3  27312  trpredeq1  27386  trpredeq2  27387  trpredeq3  27388  wrecseq123  27420  nofulllem1  27545  nofulllem2  27546  unisnif  27658  brapply  27671  ordcmp  27996  ptrest  28096  mblfinlem2  28100  ovoliunnfl  28104  voliunnfl  28106  volsupnfl  28107  isfne  28211  fnemeet2  28259  fnejoin2  28261  tailfval  28264  aomclem8  29087  dfac21  29092  stoweidlem39  29508  gsumXcom2  30507  csbfv12gALTOLD  31135  mapdunirnN  34732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rex 2700  df-uni 4067
  Copyright terms: Public domain W3C validator