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

Theorem unieqd 4028
Description: Deduction of equality of two class unions. (Contributed by NM, 21-Apr-1995.)
Hypothesis
Ref Expression
unieqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
unieqd  |-  ( ph  ->  U. A  =  U. B )

Proof of Theorem unieqd
StepHypRef Expression
1 unieqd.1 . 2  |-  ( ph  ->  A  =  B )
2 unieq 4026 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 16 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   U.cuni 4017
This theorem is referenced by:  uniprg  4032  unisng  4034  unisn2  4713  unisn3  4714  ordunisuc  4814  orduniss2  4815  onsucuni2  4816  opswap  5358  elxp4  5359  elxp5  5360  unixpid  5406  iotaeq  5428  iotabi  5429  uniabio  5430  iotanul  5435  csbfv12gALT  5741  funfv  5792  funfv2  5793  fvun  5795  dffv2  5798  fniunfv  5996  1stval  6353  2ndval  6354  fo1st  6368  fo2nd  6369  f1stres  6370  f2ndres  6371  1st2val  6374  2nd2val  6375  2nd1st  6394  cnvf1olem  6446  brtpos2  6487  dftpos4  6500  tpostpos  6501  recseq  6636  tz7.44-2  6667  tz7.44-3  6668  rdglim2  6692  ixpsnf1o  7104  xpcomco  7200  xpassen  7204  xpdom2  7205  supeq1  7452  supeq2  7455  supeq3  7456  supeq123d  7457  rankuni  7791  dfac2a  8012  dfac12lem1  8025  dfac12r  8028  kmlem9  8040  kmlem11  8042  kmlem12  8043  enfin2i  8203  fin23lem29  8223  fin23lem30  8224  fin23lem32  8226  fin23lem34  8228  fin23lem35  8229  fin23lem36  8230  fin23lem38  8231  fin23lem39  8232  fin23lem41  8234  isf34lem7  8261  isf34lem6  8262  fin1a2lem10  8291  fin1a2lem11  8292  fin1a2lem12  8293  itunisuc  8301  itunitc  8303  ttukeylem3  8393  ttukey2g  8398  pwcfsdom  8460  gruurn  8675  dfinfmr  9987  fsumcnv  12559  xpnnenOLD  12811  mrcun  13849  isacs1i  13884  mreacs  13885  arwval  14200  ipoval  14582  isacs5lem  14597  acsdrscl  14598  acsficl  14599  isps  14636  spwval2  14658  isdir  14679  gsumcom2  15551  dmdprd  15561  dprddisj  15569  dprdf1o  15592  dprdsn  15596  dprd2da  15602  dprd2db  15603  dmdprdsplit2lem  15605  lspuni0  16088  lss0v  16094  zrhval  16791  zrhval2  16792  zrhpropd  16798  isbasisg  17014  basis1  17017  baspartn  17021  tgval  17022  eltg  17024  ntrfval  17090  ntrval  17102  tgrest  17225  restuni2  17233  lmfval  17298  cnfval  17299  cnpfval  17300  pnrmopn  17409  fiuncmp  17469  cmpfi  17473  ptval  17604  ptpjpre1  17605  elptr2  17608  ptuni2  17610  ptbasin  17611  ptbasfi  17615  xkoval  17621  txtopon  17625  ptuni  17628  ptunimpt  17629  xkouni  17633  ptpjcn  17645  ptcld  17647  dfac14  17652  ptcnp  17656  prdstopn  17662  ptrescn  17673  txcmplem2  17676  xkoptsub  17688  xkopt  17689  qtopval  17729  qtopeu  17750  hmphindis  17831  txswaphmeolem  17838  ptuncnv  17841  ptunhmeo  17842  xpstopnlem1  17843  flimval  17997  fcfval  18067  alexsubALTlem3  18082  ptcmplem1  18085  ptcmplem2  18086  ptcmplem3  18087  ptcmplem4  18088  ptcmpg  18090  cnextfres  18101  cldsubg  18142  utopval  18264  tusval  18298  tuslem  18299  tususs  18302  ucnval  18309  prdsxmslem2  18561  ishtpy  18999  pi1buni  19067  pi1xfrcnv  19084  cmetcusp  19310  elovolmr  19374  ovoliunlem3  19402  uniioombllem2  19477  uniioombllem3  19479  dyadmbl  19494  vmaval  20898  vmappw  20901  disjabrex  24026  disjabrexf  24027  1stnpr  24095  2ndnpr  24096  xrge0tsmseq  24227  pstmval  24292  pstmfval  24293  esumeq12dvaf  24430  esumeq2  24435  esumval  24443  esumf1o  24447  esumsn  24458  esumss  24464  esumpfinval  24467  esumpfinvalf  24468  sxsigon  24548  meascnbl  24575  brae  24594  braew  24595  faeval  24599  imambfm  24614  cnmbfm  24615  dya2iocuni  24635  elprob  24669  probfinmeasb  24689  probmeasb  24690  dstrvprob  24731  indispcon  24923  iscvm  24948  cvmscld  24962  relexp0  25131  relexpsucr  25132  fprodcnv  25309  rdgprc0  25423  rdgprc  25424  dfrdg2  25425  dfrdg3  25426  trpredeq1  25500  trpredeq2  25501  trpredeq3  25502  wrecseq123  25534  nofulllem1  25659  nofulllem2  25660  unisnif  25772  brapply  25785  ordcmp  26199  mblfinlem2  26246  ovoliunnfl  26250  voliunnfl  26252  volsupnfl  26253  isfne  26350  fnemeet2  26398  fnejoin2  26400  tailfval  26403  aomclem8  27138  dfac21  27143  en2other2  27361  pmtrval  27373  pmtrfv  27374  pmtrprfv  27375  stoweidlem39  27766  mapdunirnN  32510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-uni 4018
  Copyright terms: Public domain W3C validator