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

Theorem uneq2d 3918
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 3912 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cun 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728
This theorem is referenced by:  ifeq2  4230  tpeq3  4415  iununi  4744  sucprc  5943  resasplit  6214  fvun1  6411  fmptapd  6581  fndifnfp  6586  fvunsn  6589  fnsnsplit  6594  oev2  7757  oarec  7796  ralxpmap  8061  sbthlem5  8230  sbthlem6  8231  domss2  8275  domunfican  8389  fiint  8393  fodomfi  8395  pm54.43  9026  kmlem2  9175  kmlem11  9184  cdaval  9194  cdaassen  9206  ackbij1lem1  9244  fin23lem26  9349  axdc3lem4  9477  fpwwe2lem13  9666  wunex2  9762  wuncval2  9771  snunico  12506  ioojoin  12510  fzsuc  12595  fseq1p1m1  12621  fseq1m1p1  12622  fzosplitsnm1  12751  fzosplitsn  12784  fzosplitpr  12785  fzosplitprm1  12786  hashfun  13426  resunimafz0  13431  s4prop  13864  fsumm1  14688  climcndslem1  14788  fprodm1  14904  ruclem4  15169  lcmfunsnlem1  15558  lcmfunsnlem2lem1  15559  lcmfunsnlem2lem2  15560  lcmfunsnlem2  15561  lcmfunsn  15565  vdwap1  15888  setsidvald  16096  setscom  16110  mreexmrid  16511  mreexexlemd  16512  mreexexlem2d  16513  cnvtsr  17430  dprd2da  18649  dmdprdsplit2lem  18652  lspun0  19224  lbsextlem4  19376  cmpcld  21426  comppfsc  21556  trfil2  21911  cldsubg  22134  tsmsres  22167  icccmplem2  22846  uniioombllem4  23574  ppiprm  25098  chtprm  25100  pntrsumbnd2  25477  pthdlem1  26897  wwlksnext  27037  clwwlknonex2lem1  27283  difres  29751  ofpreima2  29806  fzspl  29890  ordtprsuni  30305  ordtcnvNEW  30306  carsgsigalem  30717  ballotlemfp1  30893  fsum2dsub  31025  reprsuc  31033  bnj941  31181  bnj944  31346  subfacp1lem1  31499  cvmscld  31593  mrsubvrs  31757  mclsval  31798  noextend  32156  nodenselem5  32175  nosupbnd2lem1  32198  rankaltopb  32423  rankung  32610  lindsenlbs  33737  poimirlem1  33743  poimirlem2  33744  poimirlem4  33746  poimirlem6  33748  poimirlem7  33749  poimirlem8  33750  poimirlem13  33755  poimirlem14  33756  poimirlem16  33758  poimirlem17  33759  poimirlem18  33760  poimirlem19  33761  poimirlem20  33762  poimirlem21  33763  poimirlem22  33764  poimirlem26  33768  poimirlem28  33770  poimirlem31  33773  poimirlem32  33774  lshpnel2N  34794  paddfval  35605  hdmapval  37638  diophren  37903  ioounsn  38321  iunrelexp0  38520  trclfvdecoml  38547  isotone1  38872  iunp1  39756  snunioo2  40252  snunioo1  40257  dvmptfprodlem  40677  stoweidlem11  40745  stoweidlem26  40760  fourierdlem33  40874  fzopredsuc  41861  iccpartltu  41889  iccpartgt  41891  lmod1zr  42810
  Copyright terms: Public domain W3C validator