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

Theorem uneq2d 3329
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
uneq2d  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq2 3323 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150
This theorem is referenced by:  ifeq2  3570  tpeq3  3717  iununi  3986  relcoi1  5201  resasplit  5411  fvun1  5590  fvunsn  5712  fnsnsplit  5717  oev2  6522  oarec  6560  sbthlem5  6975  sbthlem6  6976  domss2  7020  domunfican  7129  fiint  7133  fodomfi  7135  pm54.43  7633  kmlem2  7777  kmlem11  7786  cdaval  7796  cdaassen  7808  ackbij1lem1  7846  fin23lem26  7951  axdc3lem4  8079  fpwwe2lem13  8264  wunex2  8360  wuncval2  8369  snunico  10763  ioojoin  10766  fzsuc  10835  fseq1p1m1  10857  fseq1m1p1  10858  fzosplitsn  10920  hashfun  11389  fsumm1  12216  climcndslem1  12308  ruclem4  12512  vdwap1  13024  setscom  13176  mreexmrid  13545  mreexexlemd  13546  mreexexlem2d  13547  cnvtsr  14331  dprd2da  15277  dmdprdsplit2lem  15280  lspun0  15768  lbsextlem4  15914  cmpcld  17129  trfil2  17582  cldsubg  17793  tsmsres  17826  icccmplem2  18328  uniioombllem4  18941  ppiprm  20389  chtprm  20391  pntrsumbnd2  20716  fzspl  23030  ballotlemfp1  23050  fmptapd  23213  subfacp1lem1  23710  cvmscld  23804  eupath2lem3  23903  rankaltopb  24513  rankung  24796  isconc1  26006  isconc2  26007  isconc3  26008  clscnc  26010  comppfsc  26307  fndifnfp  26756  ralxpmap  26761  diophren  26896  stoweidlem11  27760  stoweidlem26  27775  s4prop  28090  bnj941  28804  bnj944  28970  lshpnel2N  29175  paddfval  29986  hdmapval  32021
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