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

Theorem unieqd 4244
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 4242 . 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 1383   U.cuni 4234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-uni 4235
This theorem is referenced by:  uniprg  4248  unisng  4250  unisn3  4251  csbuni  4262  unisn2  4573  opswap  5485  unixpid  5532  iotaeq  5549  iotabi  5550  uniabio  5551  iotanul  5556  funfv  5925  funfv2  5926  fvun  5928  dffv2  5931  fniunfv  6144  ordunisuc  6652  orduniss2  6653  onsucuni2  6654  elxp4  6729  elxp5  6730  1stval  6787  2ndval  6788  1stnpr  6789  2ndnpr  6790  fo1st  6805  fo2nd  6806  f1stres  6807  f2ndres  6808  1st2val  6811  2nd2val  6812  2nd1st  6830  cnvf1olem  6883  brtpos2  6963  dftpos4  6976  tpostpos  6977  recseq  7045  tz7.44-2  7075  tz7.44-3  7076  rdglim2  7100  ixpsnf1o  7511  xpcomco  7609  xpassen  7613  xpdom2  7614  supeq1  7907  supeq2  7910  supeq3  7911  supeq123d  7912  supval2  7917  rankuni  8284  en2other2  8390  dfac2a  8513  dfac12lem1  8526  dfac12r  8529  kmlem9  8541  kmlem11  8543  kmlem12  8544  enfin2i  8704  fin23lem29  8724  fin23lem30  8725  fin23lem32  8727  fin23lem34  8729  fin23lem35  8730  fin23lem36  8731  fin23lem38  8732  fin23lem39  8733  fin23lem41  8735  isf34lem7  8762  isf34lem6  8763  fin1a2lem10  8792  fin1a2lem11  8793  fin1a2lem12  8794  itunisuc  8802  itunitc  8804  ttukeylem3  8894  ttukey2g  8899  pwcfsdom  8961  gruurn  9179  dfinfmr  10526  fsumcnv  13567  xpnnenOLD  13820  mrcun  14896  isacs1i  14931  mreacs  14932  arwval  15244  ipoval  15658  isacs5lem  15673  acsdrscl  15674  acsficl  15675  isps  15706  isdir  15736  pmtrval  16350  pmtrfv  16351  pmtrprfv  16352  pmtrdifellem3  16377  pmtrprfval  16386  gsumcom2  16877  dmdprd  16903  dprddisj  16916  dprdf1o  16953  dprdsn  16957  dprd2da  16965  dprd2db  16966  dmdprdsplit2lem  16968  lspuni0  17530  lss0v  17536  zrhval  18418  zrhval2  18419  zrhpropd  18425  isbasisg  19321  basis1  19324  baspartn  19328  tgval  19329  eltg  19331  ntrfval  19398  ntrval  19410  tgrest  19533  restuni2  19541  lmfval  19606  cnfval  19607  cnpfval  19608  pnrmopn  19717  fiuncmp  19777  cmpfi  19781  ptval  19944  ptpjpre1  19945  elptr2  19948  ptuni2  19950  ptbasin  19951  ptbasfi  19955  xkoval  19961  txtopon  19965  ptuni  19968  ptunimpt  19969  xkouni  19973  ptpjcn  19985  ptcld  19987  dfac14  19992  ptcnp  19996  prdstopn  20002  ptrescn  20013  txcmplem2  20016  xkoptsub  20028  xkopt  20029  qtopval  20069  qtopeu  20090  hmphindis  20171  txswaphmeolem  20178  ptuncnv  20181  ptunhmeo  20182  xpstopnlem1  20183  flimval  20337  fcfval  20407  alexsubALTlem3  20422  ptcmplem1  20425  ptcmplem2  20426  ptcmplem3  20427  ptcmplem4  20428  ptcmpg  20430  cnextfres  20441  cldsubg  20482  utopval  20608  tusval  20642  tuslem  20643  tususs  20646  ucnval  20653  prdsxmslem2  20905  ishtpy  21345  pi1buni  21413  pi1xfrcnv  21430  elovolmr  21760  ovoliunlem3  21788  uniioombllem2  21865  uniioombllem3  21867  dyadmbl  21882  vmaval  23259  vmappw  23262  disjabrex  27315  disjabrexf  27316  fcnvgreu  27386  xrge0tsmseq  27650  locfinreflem  27716  locfinref  27717  pstmval  27747  pstmfval  27748  ordtprsuni  27774  esumeq12dvaf  27917  esumeq2  27922  esumval  27930  esumf1o  27934  esumsn  27945  esumss  27951  esumpfinval  27954  esumpfinvalf  27955  sxsigon  28036  meascnbl  28063  brae  28086  braew  28087  faeval  28091  imambfm  28106  cnmbfm  28107  dya2iocuni  28127  omsval  28137  omsfval  28138  oms0  28139  omsmon  28140  elprob  28221  probfinmeasb  28241  probmeasb  28242  dstrvprob  28283  indispcon  28552  iscvm  28577  cvmscld  28591  msrfval  28770  msrval  28771  mthmpps  28815  relexp0  28925  relexpsucr  28926  fprodcnv  29088  rdgprc0  29201  rdgprc  29202  dfrdg2  29203  dfrdg3  29204  trpredeq1  29278  trpredeq2  29279  trpredeq3  29280  wrecseq123  29312  nofulllem1  29437  nofulllem2  29438  unisnif  29550  brapply  29563  ordcmp  29887  ptrest  30023  mblfinlem2  30027  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  isfne  30132  fnemeet2  30160  fnejoin2  30162  tailfval  30165  aomclem8  30982  dfac21  30987  stoweidlem39  31710  csbfv12gALTOLD  33354  mapdunirnN  37117
  Copyright terms: Public domain W3C validator