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

Theorem uneq2d 3461
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 3455 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  u.  A
)  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    u. cun 3278
This theorem is referenced by:  ifeq2  3704  tpeq3  3854  iununi  4135  relcoi1  5357  resasplit  5572  fvun1  5753  fvunsn  5884  fnsnsplit  5889  oev2  6726  oarec  6764  sbthlem5  7180  sbthlem6  7181  domss2  7225  domunfican  7338  fiint  7342  fodomfi  7344  pm54.43  7843  kmlem2  7987  kmlem11  7996  cdaval  8006  cdaassen  8018  ackbij1lem1  8056  fin23lem26  8161  axdc3lem4  8289  fpwwe2lem13  8473  wunex2  8569  wuncval2  8578  snunico  10980  ioojoin  10983  fzsuc  11052  fseq1p1m1  11077  fseq1m1p1  11078  fzosplitsn  11150  hashfun  11655  s4prop  11817  fsumm1  12492  climcndslem1  12584  ruclem4  12788  vdwap1  13300  setscom  13452  mreexmrid  13823  mreexexlemd  13824  mreexexlem2d  13825  cnvtsr  14609  dprd2da  15555  dmdprdsplit2lem  15558  lspun0  16042  lbsextlem4  16188  cmpcld  17419  trfil2  17872  cldsubg  18093  tsmsres  18126  icccmplem2  18807  uniioombllem4  19431  ppiprm  20887  chtprm  20889  pntrsumbnd2  21214  eupath2lem3  21654  fmptapd  24014  fzspl  24102  sibfof  24607  ballotlemfp1  24702  subfacp1lem1  24818  cvmscld  24913  fprodm1  25243  rankaltopb  25728  rankung  26011  comppfsc  26277  fndifnfp  26627  ralxpmap  26632  diophren  26764  stoweidlem11  27627  stoweidlem26  27642  fzosplitsnm1  27991  bnj941  28849  bnj944  29015  lshpnel2N  29468  paddfval  30279  hdmapval  32314
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285
  Copyright terms: Public domain W3C validator