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

Theorem uneq2d 4118
Description: Deduction adding union to the left in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
uneq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem uneq2d
StepHypRef Expression
1 uneq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 uneq2 4112 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  cun 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-un 3918
This theorem is referenced by:  ifeq2  4448  tpeq3  4656  iununi  4997  sucprc  6242  resasplit  6524  fvun1  6730  fmptapd  6909  fndifnfp  6914  fvunsn  6917  fnsnsplit  6922  oev2  8126  oarec  8166  ralxpmap  8438  sbthlem5  8609  sbthlem6  8610  domss2  8654  domunfican  8769  fiint  8773  fodomfi  8775  pm54.43  9407  kmlem2  9555  kmlem11  9564  ackbij1lem1  9620  fin23lem26  9725  axdc3lem4  9853  fpwwe2lem13  10042  wunex2  10138  wuncval2  10147  ioounsn  12846  snunico  12848  ioojoin  12852  fzsuc  12938  fseq1p1m1  12965  fseq1m1p1  12966  fzosplitsnm1  13096  fzosplitsn  13129  fzosplitpr  13130  fzosplitprm1  13131  hashfun  13783  resunimafz0  13788  s4prop  14252  fsumm1  15086  climcndslem1  15184  fprodm1  15301  ruclem4  15567  lcmfunsnlem1  15959  lcmfunsnlem2lem1  15960  lcmfunsnlem2lem2  15961  lcmfunsnlem2  15962  lcmfunsn  15966  vdwap1  16291  setsidvald  16493  setscom  16506  mreexmrid  16893  mreexexlemd  16894  mreexexlem2d  16895  cnvtsr  17811  dprd2da  19143  dmdprdsplit2lem  19146  lspun0  19759  lbsextlem4  19909  cmpcld  21986  comppfsc  22116  trfil2  22471  cldsubg  22695  tsmsres  22728  icccmplem2  23407  uniioombllem4  24169  ppiprm  25715  chtprm  25717  pntrsumbnd2  26130  pthdlem1  27534  wwlksnext  27658  clwwlknonex2lem1  27871  iunxunsn  30305  iunxunpr  30306  difres  30337  ofpreima2  30398  fzspl  30500  tocyc01  30768  ordtprsuni  31170  ordtcnvNEW  31171  carsgsigalem  31581  ballotlemfp1  31757  fsum2dsub  31886  reprsuc  31894  bnj941  32052  bnj944  32218  subfacp1lem1  32434  cvmscld  32528  satf  32608  satfv1  32618  fmlasuc  32641  mrsubvrs  32777  mclsval  32818  noextend  33181  nodenselem5  33200  nosupbnd2lem1  33223  rankaltopb  33448  rankung  33635  lindsadd  34926  lindsenlbs  34928  poimirlem1  34934  poimirlem2  34935  poimirlem4  34937  poimirlem6  34939  poimirlem7  34940  poimirlem8  34941  poimirlem13  34946  poimirlem14  34947  poimirlem16  34949  poimirlem17  34950  poimirlem18  34951  poimirlem19  34952  poimirlem20  34953  poimirlem21  34954  poimirlem22  34955  poimirlem26  34959  poimirlem28  34961  poimirlem31  34964  poimirlem32  34965  lshpnel2N  36157  paddfval  36969  hdmapval  39000  lcmfunnnd  39164  diophren  39547  iunrelexp0  40182  trclfvdecoml  40209  isotone1  40533  iunp1  41483  snunioo1  41940  dvmptfprodlem  42377  stoweidlem11  42444  stoweidlem26  42459  fourierdlem33  42573  fzopredsuc  43671  iccpartltu  43733  iccpartgt  43735  lmod1zr  44693
  Copyright terms: Public domain W3C validator