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

Theorem uneq2d 4091
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 4085 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  cun 3878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3422  df-un 3885
This theorem is referenced by:  ifeq2  4458  tpeq3  4674  iununi  5021  sucprc  6305  resasplit  6607  fvun1  6820  fmptapd  7004  fndifnfp  7009  fvunsn  7012  fnsnsplit  7017  f1ofvswap  7134  oev2  8270  oarec  8310  ralxpmap  8597  sbthlem5  8782  sbthlem6  8783  domss2  8827  dif1en  8862  unfi  8872  domunfican  8968  fiint  8972  fodomfi  8973  pm54.43  9641  kmlem2  9789  kmlem11  9798  ackbij1lem1  9858  fin23lem26  9963  axdc3lem4  10091  fpwwe2lem12  10280  wunex2  10376  wuncval2  10385  ioounsn  13089  snunico  13091  ioojoin  13095  fzsuc  13183  fseq1p1m1  13210  fseq1m1p1  13211  fzosplitsnm1  13341  fzosplitsn  13374  fzosplitpr  13375  fzosplitprm1  13376  hashfun  14028  resunimafz0  14033  s4prop  14499  fsumm1  15339  climcndslem1  15437  fprodm1  15553  ruclem4  15819  lcmfunsnlem1  16218  lcmfunsnlem2lem1  16219  lcmfunsnlem2lem2  16220  lcmfunsnlem2  16221  lcmfunsn  16225  vdwap1  16554  setscom  16757  setsidvald  16774  mreexmrid  17170  mreexexlemd  17171  mreexexlem2d  17172  cnvtsr  18118  dprd2da  19453  dmdprdsplit2lem  19456  lspun0  20072  lbsextlem4  20222  cmpcld  22323  comppfsc  22453  trfil2  22808  cldsubg  23032  tsmsres  23065  icccmplem2  23744  uniioombllem4  24507  ppiprm  26057  chtprm  26059  pntrsumbnd2  26472  pthdlem1  27877  wwlksnext  28001  clwwlknonex2lem1  28214  iunxunsn  30649  iunxunpr  30650  difres  30682  ofpreima2  30747  fzspl  30855  tocyc01  31128  ordtprsuni  31607  ordtcnvNEW  31608  carsgsigalem  32018  ballotlemfp1  32194  fsum2dsub  32323  reprsuc  32331  bnj941  32488  bnj944  32654  fineqvac  32802  subfacp1lem1  32877  cvmscld  32971  satf  33051  satfv1  33061  fmlasuc  33084  mrsubvrs  33220  mclsval  33261  noextend  33632  nodenselem5  33654  nosupbnd2lem1  33681  rankaltopb  34044  rankung  34231  lindsadd  35533  lindsenlbs  35535  poimirlem1  35541  poimirlem2  35542  poimirlem4  35544  poimirlem6  35546  poimirlem7  35547  poimirlem8  35548  poimirlem13  35553  poimirlem14  35554  poimirlem16  35556  poimirlem17  35557  poimirlem18  35558  poimirlem19  35559  poimirlem20  35560  poimirlem21  35561  poimirlem22  35562  poimirlem26  35566  poimirlem28  35568  poimirlem31  35571  poimirlem32  35572  lshpnel2N  36762  paddfval  37574  hdmapval  39605  fzsplitnd  39751  lcmfunnnd  39780  metakunt24  39899  fsuppssind  40020  diophren  40366  iunrelexp0  41015  trclfvdecoml  41042  isotone1  41363  iunp1  42315  snunioo1  42753  dvmptfprodlem  43188  stoweidlem11  43255  stoweidlem26  43270  fourierdlem33  43384  fzopredsuc  44516  iccpartltu  44578  iccpartgt  44580  lmod1zr  45535
  Copyright terms: Public domain W3C validator