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

Theorem uneq2i 3458
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 3455 . 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 1649    u. cun 3278
This theorem is referenced by:  un4  3467  unundir  3469  difdif2  3558  difun2  3667  difdifdir  3675  dfif5  3711  qdass  3863  qdassr  3864  ssunpr  3921  iununi  4135  unidif0  4332  unisuc  4617  iunsuc  4623  onuninsuci  4779  fresaun  5573  fresaunres2  5574  fvssunirn  5713  fmptap  5882  fvsnun1  5887  funiunfv  5954  difxp1  6340  tfrlem10  6607  oarec  6764  dfdom2  7092  fodomr  7217  dfsup3OLD  7407  ranksuc  7747  kmlem3  7988  fin1a2lem10  8245  fin1a2lem12  8247  axdc3lem4  8289  prunioo  10981  facnn  11523  fac0  11524  hashun3  11613  fsum2dlem  12509  fsumiun  12555  incexclem  12571  prmreclem4  13242  strlemor1  13511  strlemor2  13512  strlemor3  13513  phlstr  13563  mreexexlem4d  13827  opsrtoslem2  16500  restcld  17190  neitr  17198  fiuncmp  17421  1stckgenlem  17538  filcon  17868  ufildr  17916  alexsubALTlem3  18033  ptcmplem1  18036  restmetu  18570  ovolfiniun  19350  unmbl  19385  volfiniun  19394  voliunlem1  19397  plyun0  20069  lgsquadlem3  21093  usgrafilem1  21378  constr3trllem3  21592  constr3pthlem1  21595  ex-un  21685  ex-pw  21690  iuninc  23964  difico  24099  subfacp1lem1  24818  cvmliftlem10  24934  fprod2dlem  25257  wfrlem13  25482  wfrlem14  25483  wfrlem16  25485  axlowdimlem3  25787  axlowdimlem17  25801  mbfresfi  26152  mapfzcons  26662  mapfzcons1  26663  diophin  26721  bnj601  28997  bnj1416  29114
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285
  Copyright terms: Public domain W3C validator