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

Theorem unieqd 4101
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 4099 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 16 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   U.cuni 4091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-uni 4092
This theorem is referenced by:  uniprg  4105  unisng  4107  unisn3  4108  csbuni  4119  unisn2  4428  opswap  5326  unixpid  5372  iotaeq  5389  iotabi  5390  uniabio  5391  iotanul  5396  funfv  5758  funfv2  5759  fvun  5761  dffv2  5764  fniunfv  5964  ordunisuc  6443  orduniss2  6444  onsucuni2  6445  elxp4  6522  elxp5  6523  1stval  6579  2ndval  6580  1stnpr  6581  2ndnpr  6582  fo1st  6596  fo2nd  6597  f1stres  6598  f2ndres  6599  1st2val  6602  2nd2val  6603  2nd1st  6619  cnvf1olem  6670  brtpos2  6751  dftpos4  6764  tpostpos  6765  recseq  6833  tz7.44-2  6863  tz7.44-3  6864  rdglim2  6888  ixpsnf1o  7303  xpcomco  7401  xpassen  7405  xpdom2  7406  supeq1  7695  supeq2  7698  supeq3  7699  supeq123d  7700  supval2  7705  rankuni  8070  en2other2  8176  dfac2a  8299  dfac12lem1  8312  dfac12r  8315  kmlem9  8327  kmlem11  8329  kmlem12  8330  enfin2i  8490  fin23lem29  8510  fin23lem30  8511  fin23lem32  8513  fin23lem34  8515  fin23lem35  8516  fin23lem36  8517  fin23lem38  8518  fin23lem39  8519  fin23lem41  8521  isf34lem7  8548  isf34lem6  8549  fin1a2lem10  8578  fin1a2lem11  8579  fin1a2lem12  8580  itunisuc  8588  itunitc  8590  ttukeylem3  8680  ttukey2g  8685  pwcfsdom  8747  gruurn  8965  dfinfmr  10307  fsumcnv  13240  xpnnenOLD  13492  mrcun  14560  isacs1i  14595  mreacs  14596  arwval  14911  ipoval  15324  isacs5lem  15339  acsdrscl  15340  acsficl  15341  isps  15372  isdir  15402  pmtrval  15957  pmtrfv  15958  pmtrprfv  15959  pmtrdifellem3  15984  pmtrprfval  15993  gsumcom2  16467  dmdprd  16480  dprddisj  16493  dprdf1o  16529  dprdsn  16533  dprd2da  16541  dprd2db  16542  dmdprdsplit2lem  16544  lspuni0  17091  lss0v  17097  zrhval  17939  zrhval2  17940  zrhpropd  17946  isbasisg  18552  basis1  18555  baspartn  18559  tgval  18560  eltg  18562  ntrfval  18628  ntrval  18640  tgrest  18763  restuni2  18771  lmfval  18836  cnfval  18837  cnpfval  18838  pnrmopn  18947  fiuncmp  19007  cmpfi  19011  ptval  19143  ptpjpre1  19144  elptr2  19147  ptuni2  19149  ptbasin  19150  ptbasfi  19154  xkoval  19160  txtopon  19164  ptuni  19167  ptunimpt  19168  xkouni  19172  ptpjcn  19184  ptcld  19186  dfac14  19191  ptcnp  19195  prdstopn  19201  ptrescn  19212  txcmplem2  19215  xkoptsub  19227  xkopt  19228  qtopval  19268  qtopeu  19289  hmphindis  19370  txswaphmeolem  19377  ptuncnv  19380  ptunhmeo  19381  xpstopnlem1  19382  flimval  19536  fcfval  19606  alexsubALTlem3  19621  ptcmplem1  19624  ptcmplem2  19625  ptcmplem3  19626  ptcmplem4  19627  ptcmpg  19629  cnextfres  19640  cldsubg  19681  utopval  19807  tusval  19841  tuslem  19842  tususs  19845  ucnval  19852  prdsxmslem2  20104  ishtpy  20544  pi1buni  20612  pi1xfrcnv  20629  cmetcusp  20866  elovolmr  20959  ovoliunlem3  20987  uniioombllem2  21063  uniioombllem3  21065  dyadmbl  21080  vmaval  22451  vmappw  22454  disjabrex  25926  disjabrexf  25927  fcnvgreu  25991  xrge0tsmseq  26255  pstmval  26322  pstmfval  26323  ordtprsuni  26349  esumeq12dvaf  26487  esumeq2  26492  esumval  26500  esumf1o  26504  esumsn  26515  esumss  26521  esumpfinval  26524  esumpfinvalf  26525  sxsigon  26606  meascnbl  26633  brae  26657  braew  26658  faeval  26662  imambfm  26677  cnmbfm  26678  dya2iocuni  26698  omsval  26708  omsfval  26709  oms0  26710  omsmon  26711  elprob  26792  probfinmeasb  26812  probmeasb  26813  dstrvprob  26854  indispcon  27123  iscvm  27148  cvmscld  27162  relexp0  27331  relexpsucr  27332  fprodcnv  27494  rdgprc0  27607  rdgprc  27608  dfrdg2  27609  dfrdg3  27610  trpredeq1  27684  trpredeq2  27685  trpredeq3  27686  wrecseq123  27718  nofulllem1  27843  nofulllem2  27844  unisnif  27956  brapply  27969  ordcmp  28293  ptrest  28425  mblfinlem2  28429  ovoliunnfl  28433  voliunnfl  28435  volsupnfl  28436  isfne  28540  fnemeet2  28588  fnejoin2  28590  tailfval  28593  aomclem8  29414  dfac21  29419  stoweidlem39  29834  csbfv12gALTOLD  31557  mapdunirnN  35295
  Copyright terms: Public domain W3C validator