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

Theorem uneq12d 3438
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 3432 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  u.  C
)  =  ( B  u.  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    u. cun 3254
This theorem is referenced by:  disjpr2  3806  diftpsn3  3873  suceq  4580  fntpg  5439  foun  5626  f1oprswap  5650  fnimapr  5719  fsnunfv  5865  fsnunres  5866  oarec  6734  ereq1  6841  mapunen  7205  cnfcomlem  7582  trcl  7590  r0weon  7820  infxpen  7822  cfsmolem  8076  cfsmo  8077  axdc3lem4  8259  ttukeylem3  8317  ttukey2g  8322  alephadd  8378  fpwwe2lem13  8443  wunex2  8539  wuncval2  8548  inar1  8576  prunioo  10950  fztp  11027  fzsuc2  11028  fseq1p1m1  11045  s4dom  11786  setsvalg  13412  setsid  13428  prdsval  13598  imasval  13657  mreexd  13787  mreexexlemd  13789  ipoval  14500  istsr  14569  psrval  16349  ordtval  17168  ordtcnv  17180  paste  17273  consuba  17397  ptval2  17547  dfac14  17564  xkoptsub  17600  ptuncnv  17753  ptunhmeo  17754  xpstopnlem1  17755  alexsubALTlem3  17994  ustuqtop1  18185  ovolioo  19322  uniiccdif  19330  itgsplitioo  19589  limcfval  19619  lhop2  19759  lgsquadlem2  20999  constr3pthlem1  21483  constr3pthlem2  21484  vdgrun  21513  vdgrfiun  21514  ex-res  21590  rnpropg  23871  imadifxp  23874  probun  24449  cvmliftlem10  24753  sbcung  24896  dfrtrcl2  24920  symdifeq1  25381  axlowdimlem13  25600  axlowdimlem15  25602  axlowdim  25607  lineunray  25788  itg2addnclem2  25951  istopclsd  26438  fzsplit1nn0  26496  diophrw  26501  eldioph2lem1  26502  eldioph2lem2  26503  diophin  26515  diophren  26558  pwssplit1  26850  pwssplit4  26853  mendval  27153  bnj1373  28730  bnj1489  28756  ldualset  29291  paddval  29963  paddcom  29978  dvafset  31169  dvaset  31170  dvhfset  31246  dvhset  31247  hdmapfval  31996  hlhilset  32103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-un 3261
  Copyright terms: Public domain W3C validator