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

Theorem uneq2d 3505
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 3499 . 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 1369    u. cun 3321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328
This theorem is referenced by:  ifeq2  3791  tpeq3  3960  iununi  4250  relcoi1  5361  resasplit  5576  fvun1  5757  fmptapd  5897  fndifnfp  5902  fvunsn  5905  fnsnsplit  5910  oev2  6955  oarec  6993  ralxpmap  7254  sbthlem5  7417  sbthlem6  7418  domss2  7462  domunfican  7576  fiint  7580  fodomfi  7582  pm54.43  8162  kmlem2  8312  kmlem11  8321  cdaval  8331  cdaassen  8343  ackbij1lem1  8381  fin23lem26  8486  axdc3lem4  8614  fpwwe2lem13  8801  wunex2  8897  wuncval2  8906  snunico  11404  ioojoin  11408  fzsuc  11494  fseq1p1m1  11526  fseq1m1p1  11527  fzosplitsnm1  11600  fzosplitsn  11625  hashfun  12191  s4prop  12517  fsumm1  13212  climcndslem1  13304  ruclem4  13508  vdwap1  14030  setscom  14196  mreexmrid  14573  mreexexlemd  14574  mreexexlem2d  14575  cnvtsr  15384  dprd2da  16529  dmdprdsplit2lem  16532  srgbinomlem4  16629  lspun0  17069  lbsextlem4  17219  cmpcld  18980  trfil2  19435  cldsubg  19656  tsmsresOLD  19692  tsmsres  19693  icccmplem2  20375  uniioombllem4  21041  ppiprm  22464  chtprm  22466  pntrsumbnd2  22791  eupath2lem3  23551  ofpreima2  25936  fzspl  26028  ordtprsuni  26301  ballotlemfp1  26826  subfacp1lem1  27019  cvmscld  27114  fprodm1  27428  rankaltopb  27961  rankung  28155  comppfsc  28532  diophren  29105  ioounsn  29538  stoweidlem11  29759  stoweidlem26  29774  fzosplitpr  30176  fzosplitprm1  30177  wwlknext  30309  lmod1zr  30924  bnj941  31653  bnj944  31818  lshpnel2N  32470  paddfval  33281  hdmapval  35316
  Copyright terms: Public domain W3C validator