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

Theorem uneq2i 3522
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 3519 . 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 1369    u. cun 3341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2989  df-un 3348
This theorem is referenced by:  un4  3531  unundir  3533  difdif2  3622  difun2  3773  difdifdir  3781  dfif5  3820  qdass  3989  qdassr  3990  ssunpr  4050  iununi  4270  unidif0  4480  unisuc  4810  iunsuc  4816  difxp1  5278  fresaun  5597  fresaunres2  5598  fvssunirn  5728  fmptap  5916  fvsnun1  5928  funiunfv  5980  onuninsuci  6466  tfrlem10  6861  oarec  7016  dfdom2  7350  fodomr  7477  dfsup3OLD  7709  ranksuc  8087  kmlem3  8336  fin1a2lem10  8593  fin1a2lem12  8595  axdc3lem4  8637  prunioo  11429  facnn  12068  fac0  12069  hashun3  12162  fsum2dlem  13252  fsumiun  13299  incexclem  13314  prmreclem4  13995  strlemor1  14280  strlemor2  14281  strlemor3  14282  phlstr  14334  mreexexlem4d  14600  opsrtoslem2  17581  restcld  18791  neitr  18799  fiuncmp  19022  1stckgenlem  19141  filcon  19471  ufildr  19519  alexsubALTlem3  19636  ptcmplem1  19639  restmetu  20177  ovolfiniun  20999  unmbl  21034  volfiniun  21043  voliunlem1  21046  plyun0  21680  lgsquadlem3  22710  axlowdimlem3  23205  axlowdimlem17  23219  usgrafilem1  23339  constr3trllem3  23553  constr3pthlem1  23556  ex-un  23646  ex-pw  23651  iuninc  25926  difico  26088  subfacp1lem1  27082  cvmliftlem10  27198  fprod2dlem  27506  wfrlem13  27751  wfrlem14  27752  wfrlem16  27754  mbfresfi  28457  asindmre  28498  mapfzcons  29071  mapfzcons1  29072  diophin  29130  iocunico  29605  lmod1zr  31054  bnj601  31932  bnj1416  32049
  Copyright terms: Public domain W3C validator