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

Theorem uneq2i 3326
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 3323 . 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 1623    u. cun 3150
This theorem is referenced by:  un4  3335  unundir  3337  difun2  3533  difdifdir  3541  dfif5  3577  qdass  3726  qdassr  3727  ssunpr  3776  iununi  3986  unidif0  4183  unisuc  4468  iunsuc  4474  onuninsuci  4631  fresaun  5412  fresaunres2  5413  fvssunirn  5551  fmptap  5710  fvsnun1  5715  funiunfv  5774  difxp1  6154  tfrlem10  6403  oarec  6560  dfdom2  6887  fodomr  7012  dfsup3OLD  7197  ranksuc  7537  kmlem3  7778  fin1a2lem10  8035  fin1a2lem12  8037  axdc3lem4  8079  prunioo  10764  facnn  11290  fac0  11291  hashun3  11366  fsum2dlem  12233  fsumiun  12279  incexclem  12295  prmreclem4  12966  strlemor1  13235  strlemor2  13236  strlemor3  13237  phlstr  13287  mreexexlem4d  13549  opsrtoslem2  16226  restcld  16903  fiuncmp  17131  1stckgenlem  17248  filcon  17578  ufildr  17626  alexsubALTlem3  17743  ptcmplem1  17746  ovolfiniun  18860  unmbl  18895  volfiniun  18904  voliunlem1  18907  plyun0  19579  lgsquadlem3  20595  ex-un  20811  ex-pw  20816  iuninc  23158  subfacp1lem1  23710  cvmliftlem10  23825  wfrlem13  24268  wfrlem14  24269  wfrlem16  24271  axlowdimlem3  24572  axlowdimlem17  24586  mapfzcons  26793  mapfzcons1  26794  diophin  26852  bnj601  28952  bnj1416  29069
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator