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

Theorem uneq2i 3442
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 3439 . 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 3262
This theorem is referenced by:  un4  3451  unundir  3453  difdif2  3542  difun2  3651  difdifdir  3659  dfif5  3695  qdass  3847  qdassr  3848  ssunpr  3905  iununi  4117  unidif0  4314  unisuc  4599  iunsuc  4605  onuninsuci  4761  fresaun  5555  fresaunres2  5556  fvssunirn  5695  fmptap  5863  fvsnun1  5868  funiunfv  5935  difxp1  6321  tfrlem10  6585  oarec  6742  dfdom2  7070  fodomr  7195  dfsup3OLD  7385  ranksuc  7725  kmlem3  7966  fin1a2lem10  8223  fin1a2lem12  8225  axdc3lem4  8267  prunioo  10958  facnn  11496  fac0  11497  hashun3  11586  fsum2dlem  12482  fsumiun  12528  incexclem  12544  prmreclem4  13215  strlemor1  13484  strlemor2  13485  strlemor3  13486  phlstr  13536  mreexexlem4d  13800  opsrtoslem2  16473  restcld  17159  neitr  17167  fiuncmp  17390  1stckgenlem  17507  filcon  17837  ufildr  17885  alexsubALTlem3  18002  ptcmplem1  18005  restmetu  18490  ovolfiniun  19265  unmbl  19300  volfiniun  19309  voliunlem1  19312  plyun0  19984  lgsquadlem3  21008  usgrafilem1  21292  constr3trllem3  21488  constr3pthlem1  21491  ex-un  21581  ex-pw  21586  iuninc  23856  difico  23983  subfacp1lem1  24645  cvmliftlem10  24761  wfrlem13  25293  wfrlem14  25294  wfrlem16  25296  axlowdimlem3  25598  axlowdimlem17  25612  mapfzcons  26464  mapfzcons1  26465  diophin  26523  bnj601  28630  bnj1416  28747
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269
  Copyright terms: Public domain W3C validator