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

Theorem unieqd 4248
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 4246 . 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 1374   U.cuni 4238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-uni 4239
This theorem is referenced by:  uniprg  4252  unisng  4254  unisn3  4255  csbuni  4266  unisn2  4576  opswap  5486  unixpid  5533  iotaeq  5550  iotabi  5551  uniabio  5552  iotanul  5557  funfv  5925  funfv2  5926  fvun  5928  dffv2  5931  fniunfv  6138  ordunisuc  6638  orduniss2  6639  onsucuni2  6640  elxp4  6718  elxp5  6719  1stval  6776  2ndval  6777  1stnpr  6778  2ndnpr  6779  fo1st  6794  fo2nd  6795  f1stres  6796  f2ndres  6797  1st2val  6800  2nd2val  6801  2nd1st  6819  cnvf1olem  6871  brtpos2  6951  dftpos4  6964  tpostpos  6965  recseq  7033  tz7.44-2  7063  tz7.44-3  7064  rdglim2  7088  ixpsnf1o  7499  xpcomco  7597  xpassen  7601  xpdom2  7602  supeq1  7894  supeq2  7897  supeq3  7898  supeq123d  7899  supval2  7904  rankuni  8270  en2other2  8376  dfac2a  8499  dfac12lem1  8512  dfac12r  8515  kmlem9  8527  kmlem11  8529  kmlem12  8530  enfin2i  8690  fin23lem29  8710  fin23lem30  8711  fin23lem32  8713  fin23lem34  8715  fin23lem35  8716  fin23lem36  8717  fin23lem38  8718  fin23lem39  8719  fin23lem41  8721  isf34lem7  8748  isf34lem6  8749  fin1a2lem10  8778  fin1a2lem11  8779  fin1a2lem12  8780  itunisuc  8788  itunitc  8790  ttukeylem3  8880  ttukey2g  8885  pwcfsdom  8947  gruurn  9165  dfinfmr  10509  fsumcnv  13537  xpnnenOLD  13793  mrcun  14866  isacs1i  14901  mreacs  14902  arwval  15217  ipoval  15630  isacs5lem  15645  acsdrscl  15646  acsficl  15647  isps  15678  isdir  15708  pmtrval  16265  pmtrfv  16266  pmtrprfv  16267  pmtrdifellem3  16292  pmtrprfval  16301  gsumcom2  16787  dmdprd  16813  dprddisj  16826  dprdf1o  16862  dprdsn  16866  dprd2da  16874  dprd2db  16875  dmdprdsplit2lem  16877  lspuni0  17432  lss0v  17438  zrhval  18305  zrhval2  18306  zrhpropd  18312  isbasisg  19208  basis1  19211  baspartn  19215  tgval  19216  eltg  19218  ntrfval  19284  ntrval  19296  tgrest  19419  restuni2  19427  lmfval  19492  cnfval  19493  cnpfval  19494  pnrmopn  19603  fiuncmp  19663  cmpfi  19667  ptval  19799  ptpjpre1  19800  elptr2  19803  ptuni2  19805  ptbasin  19806  ptbasfi  19810  xkoval  19816  txtopon  19820  ptuni  19823  ptunimpt  19824  xkouni  19828  ptpjcn  19840  ptcld  19842  dfac14  19847  ptcnp  19851  prdstopn  19857  ptrescn  19868  txcmplem2  19871  xkoptsub  19883  xkopt  19884  qtopval  19924  qtopeu  19945  hmphindis  20026  txswaphmeolem  20033  ptuncnv  20036  ptunhmeo  20037  xpstopnlem1  20038  flimval  20192  fcfval  20262  alexsubALTlem3  20277  ptcmplem1  20280  ptcmplem2  20281  ptcmplem3  20282  ptcmplem4  20283  ptcmpg  20285  cnextfres  20296  cldsubg  20337  utopval  20463  tusval  20497  tuslem  20498  tususs  20501  ucnval  20508  prdsxmslem2  20760  ishtpy  21200  pi1buni  21268  pi1xfrcnv  21285  cmetcusp  21522  elovolmr  21615  ovoliunlem3  21643  uniioombllem2  21720  uniioombllem3  21722  dyadmbl  21737  vmaval  23108  vmappw  23111  disjabrex  27102  disjabrexf  27103  fcnvgreu  27172  xrge0tsmseq  27426  pstmval  27496  pstmfval  27497  ordtprsuni  27523  esumeq12dvaf  27670  esumeq2  27675  esumval  27683  esumf1o  27687  esumsn  27698  esumss  27704  esumpfinval  27707  esumpfinvalf  27708  sxsigon  27789  meascnbl  27816  brae  27839  braew  27840  faeval  27844  imambfm  27859  cnmbfm  27860  dya2iocuni  27880  omsval  27890  omsfval  27891  oms0  27892  omsmon  27893  elprob  27974  probfinmeasb  27994  probmeasb  27995  dstrvprob  28036  indispcon  28305  iscvm  28330  cvmscld  28344  relexp0  28513  relexpsucr  28514  fprodcnv  28676  rdgprc0  28789  rdgprc  28790  dfrdg2  28791  dfrdg3  28792  trpredeq1  28866  trpredeq2  28867  trpredeq3  28868  wrecseq123  28900  nofulllem1  29025  nofulllem2  29026  unisnif  29138  brapply  29151  ordcmp  29475  ptrest  29612  mblfinlem2  29616  ovoliunnfl  29620  voliunnfl  29622  volsupnfl  29623  isfne  29727  fnemeet2  29775  fnejoin2  29777  tailfval  29780  aomclem8  30600  dfac21  30605  stoweidlem39  31294  csbfv12gALTOLD  32576  mapdunirnN  36322
  Copyright terms: Public domain W3C validator