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

Theorem uneq12d 3330
Description: Equality deduction for union of two classes. (Contributed by NM, 29-Sep-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Hypotheses
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
uneq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
uneq12d  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )

Proof of Theorem uneq12d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 uneq12 3324 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150
This theorem is referenced by:  suceq  4457  foun  5491  f1oprswap  5515  fnimapr  5583  fsnunfv  5720  fsnunres  5721  oarec  6560  ereq1  6667  mapunen  7030  cnfcomlem  7402  trcl  7410  r0weon  7640  infxpen  7642  cfsmolem  7896  cfsmo  7897  axdc3lem4  8079  ttukeylem3  8138  ttukey2g  8143  alephadd  8199  fpwwe2lem13  8264  wunex2  8360  wuncval2  8369  inar1  8397  prunioo  10764  fztp  10841  fzsuc2  10842  fseq1p1m1  10857  setsvalg  13171  setsid  13187  prdsval  13355  imasval  13414  mreexd  13544  mreexexlemd  13546  ipoval  14257  istsr  14326  psrval  16110  ordtval  16919  ordtcnv  16931  paste  17022  consuba  17146  ptval2  17296  dfac14  17312  xkoptsub  17348  ptuncnv  17498  ptunhmeo  17499  xpstopnlem1  17500  alexsubALTlem3  17743  ovolioo  18925  uniiccdif  18933  itgsplitioo  19192  limcfval  19222  lhop2  19362  lgsquadlem2  20594  ex-res  20828  rnpropg  23189  probun  23622  cvmliftlem10  23825  vdgrun  23893  sbcung  24020  dfrtrcl2  24045  symdifeq1  24364  axlowdimlem13  24582  axlowdimlem15  24584  axlowdim  24589  lineunray  24770  sssu  25141  vtarsu  25886  isconc1  26006  isconc2  26007  isconc3  26008  isray2  26153  isray  26154  istopclsd  26775  fzsplit1nn0  26833  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  diophin  26852  diophren  26896  pwssplit1  27188  pwssplit4  27191  mendval  27491  difprsneq  28068  difprsng  28069  diftpsneq  28070  s4dom  28092  bnj1373  29060  bnj1489  29086  ldualset  29315  paddval  29987  paddcom  30002  dvafset  31193  dvaset  31194  dvhfset  31270  dvhset  31271  hdmapfval  32020  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator