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

Theorem unieqd 4173
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 4171 . 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 1399   U.cuni 4163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164
This theorem is referenced by:  uniprg  4177  unisng  4179  unisn3  4180  csbuni  4191  unisn2  4501  opswap  5403  unixpid  5451  iotaeq  5468  iotabi  5469  uniabio  5470  iotanul  5475  funfv  5841  funfv2  5842  fvun  5844  dffv2  5847  fniunfv  6060  ordunisuc  6566  orduniss2  6567  onsucuni2  6568  elxp4  6643  elxp5  6644  1stval  6701  2ndval  6702  1stnpr  6703  2ndnpr  6704  fo1st  6719  fo2nd  6720  f1stres  6721  f2ndres  6722  1st2val  6725  2nd2val  6726  2nd1st  6744  cnvf1olem  6797  brtpos2  6879  dftpos4  6892  tpostpos  6893  recseq  6961  tz7.44-2  6991  tz7.44-3  6992  rdglim2  7016  ixpsnf1o  7428  xpcomco  7526  xpassen  7530  xpdom2  7531  supeq1  7819  supeq2  7822  supeq3  7823  supeq123d  7824  supval2  7829  rankuni  8194  en2other2  8300  dfac2a  8423  dfac12lem1  8436  dfac12r  8439  kmlem9  8451  kmlem11  8453  kmlem12  8454  enfin2i  8614  fin23lem29  8634  fin23lem30  8635  fin23lem32  8637  fin23lem34  8639  fin23lem35  8640  fin23lem36  8641  fin23lem38  8642  fin23lem39  8643  fin23lem41  8645  isf34lem7  8672  isf34lem6  8673  fin1a2lem10  8702  fin1a2lem11  8703  fin1a2lem12  8704  itunisuc  8712  itunitc  8714  ttukeylem3  8804  ttukey2g  8809  pwcfsdom  8871  gruurn  9087  dfinfmr  10436  relexpfld  12884  fsumcnv  13590  fprodcnv  13789  mrcun  15029  isacs1i  15064  mreacs  15065  arwval  15439  ipoval  15901  isacs5lem  15916  acsdrscl  15917  acsficl  15918  isps  15949  isdir  15979  pmtrval  16593  pmtrfv  16594  pmtrprfv  16595  pmtrdifellem3  16620  pmtrprfval  16629  gsumcom2  17117  dmdprd  17142  dprddisj  17155  dprdf1o  17192  dprdsn  17196  dprd2da  17204  dprd2db  17205  dmdprdsplit2lem  17207  lspuni0  17769  lss0v  17775  zrhval  18638  zrhval2  18639  zrhpropd  18645  isbasisg  19533  basis1  19536  baspartn  19540  tgval  19541  eltg  19543  ntrfval  19610  ntrval  19622  tgrest  19746  restuni2  19754  lmfval  19819  cnfval  19820  cnpfval  19821  pnrmopn  19930  fiuncmp  19990  cmpfi  19994  ptval  20156  ptpjpre1  20157  elptr2  20160  ptuni2  20162  ptbasin  20163  ptbasfi  20167  xkoval  20173  txtopon  20177  ptuni  20180  ptunimpt  20181  xkouni  20185  ptpjcn  20197  ptcld  20199  dfac14  20204  ptcnp  20208  prdstopn  20214  ptrescn  20225  txcmplem2  20228  xkoptsub  20240  xkopt  20241  qtopval  20281  qtopeu  20302  hmphindis  20383  txswaphmeolem  20390  ptuncnv  20393  ptunhmeo  20394  xpstopnlem1  20395  flimval  20549  fcfval  20619  alexsubALTlem3  20634  ptcmplem1  20637  ptcmplem2  20638  ptcmplem3  20639  ptcmplem4  20640  ptcmpg  20642  cnextfres  20653  cldsubg  20694  utopval  20820  tusval  20854  tuslem  20855  tususs  20858  ucnval  20865  prdsxmslem2  21117  ishtpy  21557  pi1buni  21625  pi1xfrcnv  21642  elovolmr  21972  ovoliunlem3  22000  uniioombllem2  22077  uniioombllem3  22079  dyadmbl  22094  vmaval  23504  vmappw  23507  disjabrex  27572  disjabrexf  27573  fcnvgreu  27660  xrge0tsmseq  27931  locfinreflem  27997  locfinref  27998  pstmval  28028  pstmfval  28029  ordtprsuni  28055  esumeq12dvaf  28179  esumeq2  28184  esumval  28194  esumf1o  28198  esumsnf  28212  esumss  28220  esumpfinval  28223  esumpfinvalf  28224  sigapildsys  28307  sxsigon  28319  meascnbl  28346  brae  28369  braew  28370  faeval  28374  imambfm  28389  cnmbfm  28390  dya2iocuni  28410  omsval  28420  omsfval  28421  omsf  28423  oms0  28424  omssubaddlem  28426  omssubadd  28427  carsgval  28430  carsgclctunlem3  28447  omsmeas  28450  elprob  28531  probfinmeasb  28551  probmeasb  28552  dstrvprob  28593  indispcon  28868  iscvm  28893  cvmscld  28907  msrfval  29086  msrval  29087  mthmpps  29131  rdgprc0  29391  rdgprc  29392  dfrdg2  29393  dfrdg3  29394  trpredeq1  29468  trpredeq2  29469  trpredeq3  29470  wrecseq123  29502  nofulllem1  29627  nofulllem2  29628  unisnif  29728  brapply  29741  ordcmp  30065  ptrest  30213  mblfinlem2  30217  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  isfne  30323  fnemeet2  30351  fnejoin2  30353  tailfval  30356  aomclem8  31173  dfac21  31178  stoweidlem39  31987  csbfv12gALTOLD  33963  mapdunirnN  37790
  Copyright terms: Public domain W3C validator