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

Theorem unieqd 3854
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 3852 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 15 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   U.cuni 3843
This theorem is referenced by:  uniprg  3858  unisng  3860  unisn2  4538  unisn3  4539  ordunisuc  4639  orduniss2  4640  onsucuni2  4641  opswap  5175  elxp4  5176  elxp5  5177  unixpid  5223  iotaeq  5243  iotabi  5244  uniabio  5245  iotanul  5250  csbfv12gALT  5552  funfv  5602  funfv2  5603  fvun  5605  dffv2  5608  fniunfv  5789  1stval  6140  2ndval  6141  fo1st  6155  fo2nd  6156  f1stres  6157  f2ndres  6158  1st2val  6161  2nd2val  6162  2nd1st  6181  cnvf1olem  6232  brtpos2  6256  dftpos4  6269  tpostpos  6270  recseq  6405  tz7.44-2  6436  tz7.44-3  6437  rdglim2  6461  ixpsnf1o  6872  xpcomco  6968  xpassen  6972  xpdom2  6973  supeq1  7214  supeq2  7217  rankuni  7551  dfac2a  7772  dfac12lem1  7785  dfac12r  7788  kmlem9  7800  kmlem11  7802  kmlem12  7803  enfin2i  7963  fin23lem29  7983  fin23lem30  7984  fin23lem32  7986  fin23lem34  7988  fin23lem35  7989  fin23lem36  7990  fin23lem38  7991  fin23lem39  7992  fin23lem41  7994  isf34lem7  8021  isf34lem6  8022  fin1a2lem10  8051  fin1a2lem11  8052  fin1a2lem12  8053  itunisuc  8061  itunitc  8063  ttukeylem3  8154  ttukey2g  8159  pwcfsdom  8221  gruurn  8436  dfinfmr  9747  fsumcnv  12252  xpnnenOLD  12504  mrcun  13540  isacs1i  13575  mreacs  13576  arwval  13891  ipoval  14273  isacs5lem  14288  acsdrscl  14289  acsficl  14290  isps  14327  spwval2  14349  isdir  14370  gsumcom2  15242  dmdprd  15252  dprddisj  15260  dprdf1o  15283  dprdsn  15287  dprd2da  15293  dprd2db  15294  dmdprdsplit2lem  15296  lspuni0  15783  lss0v  15789  zrhval  16478  zrhval2  16479  zrhpropd  16485  isbasisg  16701  basis1  16704  baspartn  16708  tgval  16709  eltg  16711  ntrfval  16777  ntrval  16789  tgrest  16906  restuni2  16914  lmfval  16978  cnfval  16979  cnpfval  16980  pnrmopn  17087  fiuncmp  17147  cmpfi  17151  ptval  17281  ptpjpre1  17282  elptr2  17285  ptuni2  17287  ptbasin  17288  ptbasfi  17292  xkoval  17298  txtopon  17302  ptuni  17305  ptunimpt  17306  xkouni  17310  ptpjcn  17321  ptcld  17323  dfac14  17328  ptcnp  17332  prdstopn  17338  ptrescn  17349  txcmplem2  17352  xkoptsub  17364  xkopt  17365  qtopval  17402  qtopeu  17423  hmphindis  17504  txswaphmeolem  17511  ptuncnv  17514  ptunhmeo  17515  xpstopnlem1  17516  flimval  17674  fcfval  17744  alexsubALTlem3  17759  ptcmplem1  17762  ptcmplem2  17763  ptcmplem3  17764  ptcmplem4  17765  ptcmpg  17767  cldsubg  17809  prdsxmslem2  18091  ishtpy  18486  pi1buni  18554  pi1xfrcnv  18571  elovolmr  18851  ovoliunlem3  18879  uniioombllem2  18954  uniioombllem3  18956  dyadmbl  18971  vmaval  20367  vmappw  20370  1stnpr  23260  2ndnpr  23261  disjabrex  23374  disjabrexf  23375  xrge0tsmseq  23399  esumeq12dvaf  23429  esumeq2  23433  esumval  23440  esumf1o  23444  esumsn  23452  esumss  23455  esumpfinval  23458  esumpfinvalf  23459  sxsigon  23538  meascnbl  23561  imambfm  23582  cnmbfm  23583  isibfm  23608  elprob  23627  probfinmeasb  23647  probmeasb  23648  dstrvprob  23687  indispcon  23780  iscvm  23805  cvmscld  23819  relexp0  24040  relexpsucr  24041  rdgprc0  24221  rdgprc  24222  dfrdg2  24223  dfrdg3  24224  trpredeq1  24294  trpredeq2  24295  trpredeq3  24296  nofulllem1  24427  nofulllem2  24428  unisnif  24535  brapply  24548  bpolylem  24855  ordcmp  24958  ovoliunnfl  25001  isprsr  25327  ubos  25359  mxlelt  25367  mnlelt2  25369  isdir2  25395  usptoplem  25649  istopx  25650  istopxc  25651  usptop  25653  prcnt  25654  unexun  25672  supexr  25734  vtarl  25990  isfne  26371  fnemeet2  26419  fnejoin2  26421  tailfval  26424  supeq123d  27261  aomclem8  27262  dfac21  27267  en2other2  27485  pmtrval  27497  pmtrfv  27498  pmtrprfv  27499  stoweidlem39  27891  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-uni 3844
  Copyright terms: Public domain W3C validator