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

Theorem unieqd 4027
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 4025 . 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 4016
This theorem is referenced by:  uniprg  4031  unisng  4033  unisn2  4712  unisn3  4713  ordunisuc  4813  orduniss2  4814  onsucuni2  4815  opswap  5357  elxp4  5358  elxp5  5359  unixpid  5405  iotaeq  5427  iotabi  5428  uniabio  5429  iotanul  5434  csbfv12gALT  5740  funfv  5791  funfv2  5792  fvun  5794  dffv2  5797  fniunfv  5995  1stval  6352  2ndval  6353  fo1st  6367  fo2nd  6368  f1stres  6369  f2ndres  6370  1st2val  6373  2nd2val  6374  2nd1st  6393  cnvf1olem  6445  brtpos2  6486  dftpos4  6499  tpostpos  6500  recseq  6635  tz7.44-2  6666  tz7.44-3  6667  rdglim2  6691  ixpsnf1o  7103  xpcomco  7199  xpassen  7203  xpdom2  7204  supeq1  7451  supeq2  7454  supeq3  7455  supeq123d  7456  rankuni  7790  dfac2a  8011  dfac12lem1  8024  dfac12r  8027  kmlem9  8039  kmlem11  8041  kmlem12  8042  enfin2i  8202  fin23lem29  8222  fin23lem30  8223  fin23lem32  8225  fin23lem34  8227  fin23lem35  8228  fin23lem36  8229  fin23lem38  8230  fin23lem39  8231  fin23lem41  8233  isf34lem7  8260  isf34lem6  8261  fin1a2lem10  8290  fin1a2lem11  8291  fin1a2lem12  8292  itunisuc  8300  itunitc  8302  ttukeylem3  8392  ttukey2g  8397  pwcfsdom  8459  gruurn  8674  dfinfmr  9986  fsumcnv  12558  xpnnenOLD  12810  mrcun  13848  isacs1i  13883  mreacs  13884  arwval  14199  ipoval  14581  isacs5lem  14596  acsdrscl  14597  acsficl  14598  isps  14635  spwval2  14657  isdir  14678  gsumcom2  15550  dmdprd  15560  dprddisj  15568  dprdf1o  15591  dprdsn  15595  dprd2da  15601  dprd2db  15602  dmdprdsplit2lem  15604  lspuni0  16087  lss0v  16093  zrhval  16790  zrhval2  16791  zrhpropd  16797  isbasisg  17013  basis1  17016  baspartn  17020  tgval  17021  eltg  17023  ntrfval  17089  ntrval  17101  tgrest  17224  restuni2  17232  lmfval  17297  cnfval  17298  cnpfval  17299  pnrmopn  17408  fiuncmp  17468  cmpfi  17472  ptval  17603  ptpjpre1  17604  elptr2  17607  ptuni2  17609  ptbasin  17610  ptbasfi  17614  xkoval  17620  txtopon  17624  ptuni  17627  ptunimpt  17628  xkouni  17632  ptpjcn  17644  ptcld  17646  dfac14  17651  ptcnp  17655  prdstopn  17661  ptrescn  17672  txcmplem2  17675  xkoptsub  17687  xkopt  17688  qtopval  17728  qtopeu  17749  hmphindis  17830  txswaphmeolem  17837  ptuncnv  17840  ptunhmeo  17841  xpstopnlem1  17842  flimval  17996  fcfval  18066  alexsubALTlem3  18081  ptcmplem1  18084  ptcmplem2  18085  ptcmplem3  18086  ptcmplem4  18087  ptcmpg  18089  cnextfres  18100  cldsubg  18141  utopval  18263  tusval  18297  tuslem  18298  tususs  18301  ucnval  18308  prdsxmslem2  18560  ishtpy  18998  pi1buni  19066  pi1xfrcnv  19083  cmetcusp  19309  elovolmr  19373  ovoliunlem3  19401  uniioombllem2  19476  uniioombllem3  19478  dyadmbl  19493  vmaval  20897  vmappw  20900  disjabrex  24025  disjabrexf  24026  1stnpr  24094  2ndnpr  24095  xrge0tsmseq  24226  pstmval  24291  pstmfval  24292  esumeq12dvaf  24429  esumeq2  24434  esumval  24442  esumf1o  24446  esumsn  24457  esumss  24463  esumpfinval  24466  esumpfinvalf  24467  sxsigon  24547  meascnbl  24574  brae  24593  braew  24594  faeval  24598  imambfm  24613  cnmbfm  24614  dya2iocuni  24634  elprob  24668  probfinmeasb  24688  probmeasb  24689  dstrvprob  24730  indispcon  24922  iscvm  24947  cvmscld  24961  relexp0  25130  relexpsucr  25131  fprodcnv  25308  rdgprc0  25422  rdgprc  25423  dfrdg2  25424  dfrdg3  25425  trpredeq1  25499  trpredeq2  25500  trpredeq3  25501  wrecseq123  25533  nofulllem1  25658  nofulllem2  25659  unisnif  25771  brapply  25784  ordcmp  26198  mblfinlem2  26245  ovoliunnfl  26249  voliunnfl  26251  volsupnfl  26252  isfne  26349  fnemeet2  26397  fnejoin2  26399  tailfval  26402  aomclem8  27137  dfac21  27142  en2other2  27360  pmtrval  27372  pmtrfv  27373  pmtrprfv  27374  stoweidlem39  27765  mapdunirnN  32449
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 2418
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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-rex 2712  df-uni 4017
  Copyright terms: Public domain W3C validator