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

Theorem uneq2d 3501
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 3495 . 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 1652    u. cun 3318
This theorem is referenced by:  ifeq2  3744  tpeq3  3894  iununi  4175  relcoi1  5398  resasplit  5613  fvun1  5794  fvunsn  5925  fnsnsplit  5930  oev2  6767  oarec  6805  sbthlem5  7221  sbthlem6  7222  domss2  7266  domunfican  7379  fiint  7383  fodomfi  7385  pm54.43  7887  kmlem2  8031  kmlem11  8040  cdaval  8050  cdaassen  8062  ackbij1lem1  8100  fin23lem26  8205  axdc3lem4  8333  fpwwe2lem13  8517  wunex2  8613  wuncval2  8622  snunico  11024  ioojoin  11027  fzsuc  11096  fseq1p1m1  11122  fseq1m1p1  11123  fzosplitsn  11195  hashfun  11700  s4prop  11862  fsumm1  12537  climcndslem1  12629  ruclem4  12833  vdwap1  13345  setscom  13497  mreexmrid  13868  mreexexlemd  13869  mreexexlem2d  13870  cnvtsr  14654  dprd2da  15600  dmdprdsplit2lem  15603  lspun0  16087  lbsextlem4  16233  cmpcld  17465  trfil2  17919  cldsubg  18140  tsmsres  18173  icccmplem2  18854  uniioombllem4  19478  ppiprm  20934  chtprm  20936  pntrsumbnd2  21261  eupath2lem3  21701  fmptapd  24061  fzspl  24149  sibfof  24654  ballotlemfp1  24749  subfacp1lem1  24865  cvmscld  24960  fprodm1  25290  rankaltopb  25824  rankung  26107  comppfsc  26387  fndifnfp  26737  ralxpmap  26742  diophren  26874  stoweidlem11  27736  stoweidlem26  27751  fzosplitsnm1  28131  bnj941  29143  bnj944  29309  lshpnel2N  29783  paddfval  30594  hdmapval  32629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325
  Copyright terms: Public domain W3C validator