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

Theorem uneq2i 3490
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 3487 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2ax-mp 8 1  |-  ( C  u.  A )  =  ( C  u.  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    u. cun 3310
This theorem is referenced by:  un4  3499  unundir  3501  difdif2  3590  difun2  3699  difdifdir  3707  dfif5  3743  qdass  3895  qdassr  3896  ssunpr  3953  iununi  4167  unidif0  4364  unisuc  4649  iunsuc  4655  onuninsuci  4812  fresaun  5606  fresaunres2  5607  fvssunirn  5746  fmptap  5915  fvsnun1  5920  funiunfv  5987  difxp1  6373  tfrlem10  6640  oarec  6797  dfdom2  7125  fodomr  7250  dfsup3OLD  7441  ranksuc  7783  kmlem3  8024  fin1a2lem10  8281  fin1a2lem12  8283  axdc3lem4  8325  prunioo  11017  facnn  11560  fac0  11561  hashun3  11650  fsum2dlem  12546  fsumiun  12592  incexclem  12608  prmreclem4  13279  strlemor1  13548  strlemor2  13549  strlemor3  13550  phlstr  13600  mreexexlem4d  13864  opsrtoslem2  16537  restcld  17228  neitr  17236  fiuncmp  17459  1stckgenlem  17577  filcon  17907  ufildr  17955  alexsubALTlem3  18072  ptcmplem1  18075  restmetu  18609  ovolfiniun  19389  unmbl  19424  volfiniun  19433  voliunlem1  19436  plyun0  20108  lgsquadlem3  21132  usgrafilem1  21417  constr3trllem3  21631  constr3pthlem1  21634  ex-un  21724  ex-pw  21729  iuninc  24003  difico  24138  subfacp1lem1  24857  cvmliftlem10  24973  fprod2dlem  25296  wfrlem13  25542  wfrlem14  25543  wfrlem16  25545  axlowdimlem3  25875  axlowdimlem17  25889  mbfresfi  26243  mapfzcons  26763  mapfzcons1  26764  diophin  26822  bnj601  29228  bnj1416  29345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317
  Copyright terms: Public domain W3C validator