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

Theorem uneq12d 3343
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 3337 . 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 1632    u. cun 3163
This theorem is referenced by:  diftpsn3  3772  suceq  4473  foun  5507  f1oprswap  5531  fnimapr  5599  fsnunfv  5736  fsnunres  5737  oarec  6576  ereq1  6683  mapunen  7046  cnfcomlem  7418  trcl  7426  r0weon  7656  infxpen  7658  cfsmolem  7912  cfsmo  7913  axdc3lem4  8095  ttukeylem3  8154  ttukey2g  8159  alephadd  8215  fpwwe2lem13  8280  wunex2  8376  wuncval2  8385  inar1  8413  prunioo  10780  fztp  10857  fzsuc2  10858  fseq1p1m1  10873  setsvalg  13187  setsid  13203  prdsval  13371  imasval  13430  mreexd  13560  mreexexlemd  13562  ipoval  14273  istsr  14342  psrval  16126  ordtval  16935  ordtcnv  16947  paste  17038  consuba  17162  ptval2  17312  dfac14  17328  xkoptsub  17364  ptuncnv  17514  ptunhmeo  17515  xpstopnlem1  17516  alexsubALTlem3  17759  ovolioo  18941  uniiccdif  18949  itgsplitioo  19208  limcfval  19238  lhop2  19378  lgsquadlem2  20610  ex-res  20844  rnpropg  23205  probun  23637  cvmliftlem10  23840  vdgrun  23908  sbcung  24035  dfrtrcl2  24060  symdifeq1  24435  axlowdimlem13  24654  axlowdimlem15  24656  axlowdim  24661  lineunray  24842  itg2addnclem2  25004  sssu  25244  vtarsu  25989  isconc1  26109  isconc2  26110  isconc3  26111  isray2  26256  isray  26257  istopclsd  26878  fzsplit1nn0  26936  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  diophin  26955  diophren  26999  pwssplit1  27291  pwssplit4  27294  mendval  27594  disjpr2  28185  s4dom  28224  constr3pthlem1  28401  constr3pthlem2  28402  bnj1373  29376  bnj1489  29402  ldualset  29937  paddval  30609  paddcom  30624  dvafset  31815  dvaset  31816  dvhfset  31892  dvhset  31893  hdmapfval  32642  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator