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

Theorem unieqd 4091
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 4089 . 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 1364   U.cuni 4081
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 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2713  df-uni 4082
This theorem is referenced by:  uniprg  4095  unisng  4097  unisn3  4098  csbuni  4109  unisn2  4418  opswap  5316  unixpid  5362  iotaeq  5379  iotabi  5380  uniabio  5381  iotanul  5386  funfv  5748  funfv2  5749  fvun  5751  dffv2  5754  fniunfv  5953  ordunisuc  6434  orduniss2  6435  onsucuni2  6436  elxp4  6513  elxp5  6514  1stval  6570  2ndval  6571  1stnpr  6572  2ndnpr  6573  fo1st  6587  fo2nd  6588  f1stres  6589  f2ndres  6590  1st2val  6593  2nd2val  6594  2nd1st  6610  cnvf1olem  6661  brtpos2  6742  dftpos4  6755  tpostpos  6756  recseq  6821  tz7.44-2  6851  tz7.44-3  6852  rdglim2  6876  ixpsnf1o  7293  xpcomco  7391  xpassen  7395  xpdom2  7396  supeq1  7685  supeq2  7688  supeq3  7689  supeq123d  7690  supval2  7695  rankuni  8060  en2other2  8166  dfac2a  8289  dfac12lem1  8302  dfac12r  8305  kmlem9  8317  kmlem11  8319  kmlem12  8320  enfin2i  8480  fin23lem29  8500  fin23lem30  8501  fin23lem32  8503  fin23lem34  8505  fin23lem35  8506  fin23lem36  8507  fin23lem38  8508  fin23lem39  8509  fin23lem41  8511  isf34lem7  8538  isf34lem6  8539  fin1a2lem10  8568  fin1a2lem11  8569  fin1a2lem12  8570  itunisuc  8578  itunitc  8580  ttukeylem3  8670  ttukey2g  8675  pwcfsdom  8737  gruurn  8955  dfinfmr  10297  fsumcnv  13226  xpnnenOLD  13477  mrcun  14545  isacs1i  14580  mreacs  14581  arwval  14896  ipoval  15309  isacs5lem  15324  acsdrscl  15325  acsficl  15326  isps  15357  isdir  15387  pmtrval  15939  pmtrfv  15940  pmtrprfv  15941  pmtrdifellem3  15966  pmtrprfval  15975  gsumcom2  16443  dmdprd  16456  dprddisj  16469  dprdf1o  16505  dprdsn  16509  dprd2da  16517  dprd2db  16518  dmdprdsplit2lem  16520  lspuni0  17015  lss0v  17021  zrhval  17783  zrhval2  17784  zrhpropd  17790  isbasisg  18396  basis1  18399  baspartn  18403  tgval  18404  eltg  18406  ntrfval  18472  ntrval  18484  tgrest  18607  restuni2  18615  lmfval  18680  cnfval  18681  cnpfval  18682  pnrmopn  18791  fiuncmp  18851  cmpfi  18855  ptval  18987  ptpjpre1  18988  elptr2  18991  ptuni2  18993  ptbasin  18994  ptbasfi  18998  xkoval  19004  txtopon  19008  ptuni  19011  ptunimpt  19012  xkouni  19016  ptpjcn  19028  ptcld  19030  dfac14  19035  ptcnp  19039  prdstopn  19045  ptrescn  19056  txcmplem2  19059  xkoptsub  19071  xkopt  19072  qtopval  19112  qtopeu  19133  hmphindis  19214  txswaphmeolem  19221  ptuncnv  19224  ptunhmeo  19225  xpstopnlem1  19226  flimval  19380  fcfval  19450  alexsubALTlem3  19465  ptcmplem1  19468  ptcmplem2  19469  ptcmplem3  19470  ptcmplem4  19471  ptcmpg  19473  cnextfres  19484  cldsubg  19525  utopval  19651  tusval  19685  tuslem  19686  tususs  19689  ucnval  19696  prdsxmslem2  19948  ishtpy  20388  pi1buni  20456  pi1xfrcnv  20473  cmetcusp  20710  elovolmr  20803  ovoliunlem3  20831  uniioombllem2  20907  uniioombllem3  20909  dyadmbl  20924  vmaval  22338  vmappw  22341  disjabrex  25752  disjabrexf  25753  fcnvgreu  25817  xrge0tsmseq  26110  pstmval  26178  pstmfval  26179  ordtprsuni  26205  esumeq12dvaf  26343  esumeq2  26348  esumval  26356  esumf1o  26360  esumsn  26371  esumss  26377  esumpfinval  26380  esumpfinvalf  26381  sxsigon  26462  meascnbl  26489  brae  26513  braew  26514  faeval  26518  imambfm  26533  cnmbfm  26534  dya2iocuni  26554  elprob  26642  probfinmeasb  26662  probmeasb  26663  dstrvprob  26704  indispcon  26973  iscvm  26998  cvmscld  27012  relexp0  27180  relexpsucr  27181  fprodcnv  27343  rdgprc0  27456  rdgprc  27457  dfrdg2  27458  dfrdg3  27459  trpredeq1  27533  trpredeq2  27534  trpredeq3  27535  wrecseq123  27567  nofulllem1  27692  nofulllem2  27693  unisnif  27805  brapply  27818  ordcmp  28143  ptrest  28271  mblfinlem2  28275  ovoliunnfl  28279  voliunnfl  28281  volsupnfl  28282  isfne  28386  fnemeet2  28434  fnejoin2  28436  tailfval  28439  aomclem8  29261  dfac21  29266  stoweidlem39  29682  csbfv12gALTOLD  31299  mapdunirnN  34908
  Copyright terms: Public domain W3C validator