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

Theorem uneq2i 3339
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 3336 . 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 1632    u. cun 3163
This theorem is referenced by:  un4  3348  unundir  3350  difun2  3546  difdifdir  3554  dfif5  3590  qdass  3739  qdassr  3740  ssunpr  3792  iununi  4002  unidif0  4199  unisuc  4484  iunsuc  4490  onuninsuci  4647  fresaun  5428  fresaunres2  5429  fvssunirn  5567  fmptap  5726  fvsnun1  5731  funiunfv  5790  difxp1  6170  tfrlem10  6419  oarec  6576  dfdom2  6903  fodomr  7028  dfsup3OLD  7213  ranksuc  7553  kmlem3  7794  fin1a2lem10  8051  fin1a2lem12  8053  axdc3lem4  8095  prunioo  10780  facnn  11306  fac0  11307  hashun3  11382  fsum2dlem  12249  fsumiun  12295  incexclem  12311  prmreclem4  12982  strlemor1  13251  strlemor2  13252  strlemor3  13253  phlstr  13303  mreexexlem4d  13565  opsrtoslem2  16242  restcld  16919  fiuncmp  17147  1stckgenlem  17264  filcon  17594  ufildr  17642  alexsubALTlem3  17759  ptcmplem1  17762  ovolfiniun  18876  unmbl  18911  volfiniun  18920  voliunlem1  18923  plyun0  19595  lgsquadlem3  20611  ex-un  20827  ex-pw  20832  iuninc  23174  subfacp1lem1  23725  cvmliftlem10  23840  wfrlem13  24339  wfrlem14  24340  wfrlem16  24342  axlowdimlem3  24644  axlowdimlem17  24658  mapfzcons  26896  mapfzcons1  26897  diophin  26955  constr3trllem3  28398  constr3pthlem1  28401  bnj601  29268  bnj1416  29385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator