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

Theorem uneq2d 3658
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 3652 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  ifeq2  3944  tpeq3  4117  iununi  4410  relcoi1  5534  resasplit  5753  fvun1  5936  fmptapd  6083  fndifnfp  6088  fvunsn  6091  fnsnsplit  6096  oev2  7170  oarec  7208  ralxpmap  7465  sbthlem5  7628  sbthlem6  7629  domss2  7673  domunfican  7789  fiint  7793  fodomfi  7795  pm54.43  8377  kmlem2  8527  kmlem11  8536  cdaval  8546  cdaassen  8558  ackbij1lem1  8596  fin23lem26  8701  axdc3lem4  8829  fpwwe2lem13  9016  wunex2  9112  wuncval2  9121  snunico  11643  ioojoin  11647  fzsuc  11723  fseq1p1m1  11748  fseq1m1p1  11749  fzosplitsnm1  11854  fzosplitsn  11882  fzosplitprm1  11883  hashfun  12457  s4prop  12822  fsumm1  13525  climcndslem1  13620  ruclem4  13824  vdwap1  14350  setscom  14516  mreexmrid  14894  mreexexlemd  14895  mreexexlem2d  14896  cnvtsr  15705  dprd2da  16881  dmdprdsplit2lem  16884  lspun0  17440  lbsextlem4  17590  cmpcld  19668  trfil2  20123  cldsubg  20344  tsmsresOLD  20380  tsmsres  20381  icccmplem2  21063  uniioombllem4  21730  ppiprm  23153  chtprm  23155  pntrsumbnd2  23480  wwlknext  24400  eupath2lem3  24655  difres  27130  ofpreima2  27180  fzspl  27266  ordtprsuni  27537  ballotlemfp1  28070  subfacp1lem1  28263  cvmscld  28358  fprodm1  28673  rankaltopb  29206  rankung  29400  comppfsc  29779  diophren  30351  ioounsn  30782  snunioo2  31108  snunioo1  31116  stoweidlem11  31311  stoweidlem26  31326  fourierdlem33  31440  fzosplitpr  31811  lmod1zr  32175  bnj941  32910  bnj944  33075  lshpnel2N  33782  paddfval  34593  hdmapval  36628
  Copyright terms: Public domain W3C validator