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

Theorem unieqd 4229
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 4227 . 2  |-  ( A  =  B  ->  U. A  =  U. B )
31, 2syl 17 1  |-  ( ph  ->  U. A  =  U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   U.cuni 4219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777  df-uni 4220
This theorem is referenced by:  uniprg  4233  unisng  4235  unisn3  4236  csbuni  4247  unisn2  4560  opswap  5342  unixpid  5390  iotaeq  5573  iotabi  5574  uniabio  5575  iotanul  5580  funfv  5948  funfv2  5949  fvun  5951  dffv2  5954  fniunfv  6167  ordunisuc  6673  orduniss2  6674  onsucuni2  6675  elxp4  6751  elxp5  6752  1stval  6809  2ndval  6810  1stnpr  6811  2ndnpr  6812  fo1st  6827  fo2nd  6828  f1stres  6829  f2ndres  6830  1st2val  6833  2nd2val  6834  2nd1st  6852  cnvf1olem  6905  brtpos2  6990  dftpos4  7003  tpostpos  7004  wrecseq123  7040  tz7.44-2  7136  tz7.44-3  7137  rdglim2  7161  ixpsnf1o  7573  xpcomco  7671  xpassen  7675  xpdom2  7676  supeq1  7968  supeq2  7971  supeq3  7972  supeq123d  7973  supval2  7978  rankuni  8342  en2other2  8448  dfac2a  8567  dfac12lem1  8580  dfac12r  8583  kmlem9  8595  kmlem11  8597  kmlem12  8598  enfin2i  8758  fin23lem29  8778  fin23lem30  8779  fin23lem32  8781  fin23lem34  8783  fin23lem35  8784  fin23lem36  8785  fin23lem38  8786  fin23lem39  8787  fin23lem41  8789  isf34lem7  8816  isf34lem6  8817  fin1a2lem10  8846  fin1a2lem11  8847  fin1a2lem12  8848  itunisuc  8856  itunitc  8858  ttukeylem3  8948  ttukey2g  8953  pwcfsdom  9015  gruurn  9230  dfinfre  10595  dfinfmrOLD  10596  relexpfld  13112  fsumcnv  13833  fprodcnv  14036  mrcun  15527  isacs1i  15562  mreacs  15563  arwval  15937  ipoval  16399  isacs5lem  16414  acsdrscl  16415  acsficl  16416  isps  16447  isdir  16477  pmtrval  17091  pmtrfv  17092  pmtrprfv  17093  pmtrdifellem3  17118  pmtrprfval  17127  gsumcom2  17606  dmdprd  17629  dprddisj  17640  dprdf1o  17664  dprdsn  17668  dprd2da  17674  dprd2db  17675  dmdprdsplit2lem  17677  lspuni0  18232  lss0v  18238  zrhval  19077  zrhval2  19078  zrhpropd  19084  isbasisg  19960  basis1  19963  baspartn  19967  tgval  19968  eltg  19970  ntrfval  20037  ntrval  20049  tgrest  20173  restuni2  20181  lmfval  20246  cnfval  20247  cnpfval  20248  pnrmopn  20357  fiuncmp  20417  cmpfi  20421  ptval  20583  ptpjpre1  20584  elptr2  20587  ptuni2  20589  ptbasin  20590  ptbasfi  20594  xkoval  20600  txtopon  20604  ptuni  20607  ptunimpt  20608  xkouni  20612  ptpjcn  20624  ptcld  20626  dfac14  20631  ptcnp  20635  prdstopn  20641  ptrescn  20652  txcmplem2  20655  xkoptsub  20667  xkopt  20668  qtopval  20708  qtopeu  20729  hmphindis  20810  txswaphmeolem  20817  ptuncnv  20820  ptunhmeo  20821  xpstopnlem1  20822  flimval  20976  fcfval  21046  alexsubALTlem3  21062  ptcmplem1  21065  ptcmplem2  21066  ptcmplem3  21067  ptcmplem4  21068  ptcmpg  21070  cnextfres1  21081  cldsubg  21123  utopval  21245  tusval  21279  tuslem  21280  tususs  21283  ucnval  21290  prdsxmslem2  21542  ishtpy  22001  pi1buni  22069  pi1xfrcnv  22086  elovolmr  22427  ovoliunlem3  22455  uniioombllem2  22538  uniioombllem2OLD  22539  uniioombllem3  22541  dyadmbl  22556  vmaval  24038  vmappw  24041  disjabrex  28194  disjabrexf  28195  fcnvgreu  28277  xrge0tsmseq  28558  locfinreflem  28675  locfinref  28676  pstmval  28706  pstmfval  28707  ordtprsuni  28733  esumeq12dvaf  28860  esumeq2  28865  esumval  28875  esumf1o  28879  esumsnf  28893  esumss  28901  esumpfinval  28904  esumpfinvalf  28905  sigapildsys  28992  sxsigon  29022  meascnbl  29049  brae  29072  braew  29073  faeval  29077  imambfm  29092  cnmbfm  29093  dya2iocuni  29113  omsval  29125  omsfval  29126  omsf  29128  omsvalOLD  29129  omsfvalOLD  29130  omsfOLD  29132  oms0  29133  omssubaddlem  29135  omssubadd  29136  oms0OLD  29137  omssubaddlemOLD  29139  omssubaddOLD  29140  carsgval  29143  carsgclctunlem3  29160  omsmeas  29163  omsmeasOLD  29164  elprob  29250  probfinmeasb  29270  probmeasb  29271  dstrvprob  29312  indispcon  29965  iscvm  29990  cvmscld  30004  msrfval  30183  msrval  30184  mthmpps  30228  rdgprc0  30447  rdgprc  30448  dfrdg2  30449  dfrdg3  30450  trpredeq1  30468  trpredeq2  30469  trpredeq3  30470  nofulllem1  30596  nofulllem2  30597  unisnif  30697  brapply  30710  isfne  31000  fnemeet2  31028  fnejoin2  31030  tailfval  31033  ordcmp  31112  csbwrecsg  31692  mptsnunlem  31704  dissneqlem  31706  ptrest  31903  mblfinlem2  31942  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  mapdunirnN  35187  aomclem8  35889  dfac21  35894  csbfv12gALTOLD  37186  stoweidlem39  37840  caragenval  38222  isome  38223  omeiunle  38246  isomennd  38260
  Copyright terms: Public domain W3C validator