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

Theorem uneq2d 3750
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 3744 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cun 3557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-un 3564
This theorem is referenced by:  ifeq2  4068  tpeq3  4254  iununi  4581  sucprc  5764  resasplit  6036  fvun1  6231  fmptapd  6397  fndifnfp  6402  fvunsn  6405  fnsnsplit  6410  oev2  7555  oarec  7594  ralxpmap  7859  sbthlem5  8026  sbthlem6  8027  domss2  8071  domunfican  8185  fiint  8189  fodomfi  8191  pm54.43  8778  kmlem2  8925  kmlem11  8934  cdaval  8944  cdaassen  8956  ackbij1lem1  8994  fin23lem26  9099  axdc3lem4  9227  fpwwe2lem13  9416  wunex2  9512  wuncval2  9521  snunico  12249  ioojoin  12253  fzsuc  12338  fseq1p1m1  12363  fseq1m1p1  12364  fzosplitsnm1  12491  fzosplitsn  12525  fzosplitprm1  12526  hashfun  13172  resunimafz0  13175  s4prop  13599  fsumm1  14421  climcndslem1  14517  fprodm1  14633  ruclem4  14899  lcmfunsnlem1  15285  lcmfunsnlem2lem1  15286  lcmfunsnlem2lem2  15287  lcmfunsnlem2  15288  lcmfunsn  15292  vdwap1  15616  setsidvald  15821  setscom  15835  mreexmrid  16235  mreexexlemd  16236  mreexexlem2d  16237  cnvtsr  17154  dprd2da  18373  dmdprdsplit2lem  18376  lspun0  18943  lbsextlem4  19093  cmpcld  21128  comppfsc  21258  trfil2  21614  cldsubg  21837  tsmsres  21870  icccmplem2  22549  uniioombllem4  23277  ppiprm  24794  chtprm  24796  pntrsumbnd2  25173  pthdlem1  26548  wwlksnext  26674  difres  29281  ofpreima2  29332  fzspl  29415  ordtprsuni  29771  ordtcnvNEW  29772  carsgsigalem  30182  ballotlemfp1  30358  breprsuc  30483  bnj941  30586  bnj944  30751  subfacp1lem1  30904  cvmscld  30998  mrsubvrs  31162  mclsval  31203  noextend  31559  noextendltgt  31609  rankaltopb  31763  rankung  31950  lindsenlbs  33071  poimirlem1  33077  poimirlem2  33078  poimirlem4  33080  poimirlem6  33082  poimirlem7  33083  poimirlem8  33084  poimirlem13  33089  poimirlem14  33090  poimirlem16  33092  poimirlem17  33093  poimirlem18  33094  poimirlem19  33095  poimirlem20  33096  poimirlem21  33097  poimirlem22  33098  poimirlem26  33102  poimirlem28  33104  poimirlem31  33107  poimirlem32  33108  lshpnel2N  33787  paddfval  34598  hdmapval  36635  diophren  36892  ioounsn  37311  iunrelexp0  37510  trclfvdecoml  37537  isotone1  37863  iunp1  38753  snunioo2  39173  snunioo1  39180  dvmptfprodlem  39492  stoweidlem11  39561  stoweidlem26  39576  fourierdlem33  39690  fzopredsuc  40656  fzosplitpr  40662  iccpartltu  40685  iccpartgt  40687  lmod1zr  41596
  Copyright terms: Public domain W3C validator