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

Theorem uneq2d 3643
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 3637 . 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 1383    u. cun 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466
This theorem is referenced by:  ifeq2  3931  tpeq3  4105  iununi  4400  relcoi1  5526  resasplit  5745  fvun1  5929  fmptapd  6080  fndifnfp  6085  fvunsn  6088  fnsnsplit  6093  oev2  7175  oarec  7213  ralxpmap  7470  sbthlem5  7633  sbthlem6  7634  domss2  7678  domunfican  7795  fiint  7799  fodomfi  7801  pm54.43  8384  kmlem2  8534  kmlem11  8543  cdaval  8553  cdaassen  8565  ackbij1lem1  8603  fin23lem26  8708  axdc3lem4  8836  fpwwe2lem13  9023  wunex2  9119  wuncval2  9128  snunico  11658  ioojoin  11662  fzsuc  11738  fseq1p1m1  11763  fseq1m1p1  11764  fzosplitsnm1  11872  fzosplitsn  11900  fzosplitprm1  11901  hashfun  12477  s4prop  12845  fsumm1  13548  climcndslem1  13643  fprodm1  13753  ruclem4  13949  vdwap1  14477  setscom  14644  mreexmrid  15022  mreexexlemd  15023  mreexexlem2d  15024  cnvtsr  15831  dprd2da  17070  dmdprdsplit2lem  17073  lspun0  17636  lbsextlem4  17786  cmpcld  19880  comppfsc  20011  trfil2  20366  cldsubg  20587  tsmsresOLD  20623  tsmsres  20624  icccmplem2  21306  uniioombllem4  21973  ppiprm  23403  chtprm  23405  pntrsumbnd2  23730  wwlknext  24702  eupath2lem3  24957  difres  27435  ofpreima2  27486  fzspl  27576  ordtprsuni  27879  ordtcnvNEW  27880  ballotlemfp1  28408  subfacp1lem1  28601  cvmscld  28696  mrsubvrs  28860  mclsval  28901  rankaltopb  29605  rankung  29799  diophren  30723  ioounsn  31153  snunioo2  31498  snunioo1  31506  dvmptfprodlem  31695  stoweidlem11  31747  stoweidlem26  31762  fourierdlem33  31876  fzosplitpr  32296  setsidvald  32508  lmod1zr  32964  bnj941  33699  bnj944  33864  lshpnel2N  34585  paddfval  35396  hdmapval  37433
  Copyright terms: Public domain W3C validator