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

Theorem uneq2d 4136
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 4130 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cun 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938
This theorem is referenced by:  ifeq2  4468  tpeq3  4672  iununi  5012  sucprc  6259  resasplit  6541  fvun1  6747  fmptapd  6925  fndifnfp  6930  fvunsn  6933  fnsnsplit  6938  oev2  8137  oarec  8177  ralxpmap  8448  sbthlem5  8619  sbthlem6  8620  domss2  8664  domunfican  8779  fiint  8783  fodomfi  8785  pm54.43  9417  kmlem2  9565  kmlem11  9574  ackbij1lem1  9630  fin23lem26  9735  axdc3lem4  9863  fpwwe2lem13  10052  wunex2  10148  wuncval2  10157  ioounsn  12851  snunico  12853  ioojoin  12857  fzsuc  12942  fseq1p1m1  12969  fseq1m1p1  12970  fzosplitsnm1  13100  fzosplitsn  13133  fzosplitpr  13134  fzosplitprm1  13135  hashfun  13786  resunimafz0  13791  s4prop  14260  fsumm1  15094  climcndslem1  15192  fprodm1  15309  ruclem4  15575  lcmfunsnlem1  15969  lcmfunsnlem2lem1  15970  lcmfunsnlem2lem2  15971  lcmfunsnlem2  15972  lcmfunsn  15976  vdwap1  16301  setsidvald  16502  setscom  16515  mreexmrid  16902  mreexexlemd  16903  mreexexlem2d  16904  cnvtsr  17820  dprd2da  19093  dmdprdsplit2lem  19096  lspun0  19712  lbsextlem4  19862  cmpcld  21938  comppfsc  22068  trfil2  22423  cldsubg  22646  tsmsres  22679  icccmplem2  23358  uniioombllem4  24114  ppiprm  25655  chtprm  25657  pntrsumbnd2  26070  pthdlem1  27474  wwlksnext  27598  clwwlknonex2lem1  27813  iunxunsn  30246  iunxunpr  30247  difres  30278  ofpreima2  30339  fzspl  30439  tocyc01  30687  ordtprsuni  31061  ordtcnvNEW  31062  carsgsigalem  31472  ballotlemfp1  31648  fsum2dsub  31777  reprsuc  31785  bnj941  31943  bnj944  32109  subfacp1lem1  32323  cvmscld  32417  satf  32497  satfv1  32507  fmlasuc  32530  mrsubvrs  32666  mclsval  32707  noextend  33070  nodenselem5  33089  nosupbnd2lem1  33112  rankaltopb  33337  rankung  33524  lindsadd  34766  lindsenlbs  34768  poimirlem1  34774  poimirlem2  34775  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem8  34781  poimirlem13  34786  poimirlem14  34787  poimirlem16  34789  poimirlem17  34790  poimirlem18  34791  poimirlem19  34792  poimirlem20  34793  poimirlem21  34794  poimirlem22  34795  poimirlem26  34799  poimirlem28  34801  poimirlem31  34804  poimirlem32  34805  lshpnel2N  36001  paddfval  36813  hdmapval  38844  diophren  39288  iunrelexp0  39925  trclfvdecoml  39952  isotone1  40276  iunp1  41205  snunioo1  41664  dvmptfprodlem  42105  stoweidlem11  42173  stoweidlem26  42188  fourierdlem33  42302  fzopredsuc  43400  iccpartltu  43462  iccpartgt  43464  lmod1zr  44476
  Copyright terms: Public domain W3C validator