MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq2i Structured version   Unicode version

Theorem uneq2i 3618
Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1  |-  A  =  B
Assertion
Ref Expression
uneq2i  |-  ( C  u.  A )  =  ( C  u.  B
)

Proof of Theorem uneq2i
StepHypRef Expression
1 uneq1i.1 . 2  |-  A  =  B
2 uneq2 3615 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2ax-mp 5 1  |-  ( C  u.  A )  =  ( C  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438    u. cun 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442
This theorem is referenced by:  un4  3627  unundir  3629  difdif2  3731  difun2  3876  difdifdir  3884  dfif5  3926  qdass  4097  qdassr  4098  ssunpr  4160  iununi  4385  unidif0  4595  difxp1  5279  unisuc  5516  iunsuc  5522  fresaun  5769  fresaunres2  5770  fvssunirn  5902  fmptap  6100  fvsnun1  6112  funiunfv  6166  onuninsuci  6679  wfrlem13  7054  wfrlem14  7055  wfrlem16  7057  tfrlem10  7111  oarec  7269  dfdom2  7600  fodomr  7727  ranksuc  8339  kmlem3  8584  fin1a2lem10  8841  fin1a2lem12  8843  axdc3lem4  8885  prunioo  11763  facnn  12462  fac0  12463  hashun3  12564  trclublem  13053  dmtrclfv  13076  fsum2dlem  13824  fsumiun  13874  incexclem  13887  fprod2dlem  14027  prmreclem4  14856  strlemor1  15210  strlemor2  15211  strlemor3  15212  phlstr  15271  mreexexlem4d  15546  opsrtoslem2  18701  restcld  20180  neitr  20188  fiuncmp  20411  refun0  20522  1stckgenlem  20560  filcon  20890  ufildr  20938  alexsubALTlem3  21056  ptcmplem1  21059  restmetu  21577  ovolfiniun  22446  unmbl  22483  volfiniun  22492  voliunlem1  22495  plyun0  23143  lgsquadlem3  24276  axlowdimlem3  24966  axlowdimlem17  24980  usgrafilem1  25131  constr3trllem3  25372  constr3pthlem1  25375  ex-un  25866  ex-pw  25871  indifundif  28145  iuninc  28172  difico  28365  esum2dlem  28915  fiunelcarsg  29150  carsgclctunlem1  29151  carsggect  29152  bnj601  29733  bnj1416  29850  subfacp1lem1  29904  cvmliftlem10  30019  poimirlem4  31902  poimirlem18  31916  poimirlem21  31919  poimirlem22  31920  poimirlem25  31923  mbfresfi  31945  asindmre  31985  mapfzcons  35521  mapfzcons1  35522  diophin  35578  iocunico  36059  rp-fakeuninass  36125  dfrcl2  36170  corcltrcl  36235  cotrclrcl  36238  frege109d  36253  frege131d  36260  fiiuncl  37313  fourierdlem65  37899  fourierdlem89  37923  fourierdlem90  37924  fourierdlem91  37925  fourierdlem96  37930  fourierdlem97  37931  fourierdlem98  37932  fourierdlem99  37933  fourierdlem100  37934  fourierdlem105  37939  fourierdlem108  37942  fourierdlem109  37943  fourierdlem110  37944  fourierdlem112  37946  fourierdlem113  37947  isomenndlem  38174  1fzopredsuc  38477  lmod1zr  39630
  Copyright terms: Public domain W3C validator