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

Theorem uneq2i 3655
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 3652 . 2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
31, 2ax-mp 5 1  |-  ( C  u.  A )  =  ( C  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  un4  3664  unundir  3666  difdif2  3755  difun2  3906  difdifdir  3914  dfif5  3955  qdass  4126  qdassr  4127  ssunpr  4189  iununi  4410  unidif0  4620  unisuc  4954  iunsuc  4960  difxp1  5430  fresaun  5754  fresaunres2  5755  fvssunirn  5887  fmptap  6082  fvsnun1  6094  funiunfv  6146  onuninsuci  6653  tfrlem10  7053  oarec  7208  dfdom2  7538  fodomr  7665  dfsup3OLD  7900  ranksuc  8279  kmlem3  8528  fin1a2lem10  8785  fin1a2lem12  8787  axdc3lem4  8829  prunioo  11645  facnn  12319  fac0  12320  hashun3  12416  fsum2dlem  13544  fsumiun  13594  incexclem  13607  prmreclem4  14292  strlemor1  14578  strlemor2  14579  strlemor3  14580  phlstr  14632  mreexexlem4d  14898  opsrtoslem2  17920  restcld  19439  neitr  19447  fiuncmp  19670  1stckgenlem  19789  filcon  20119  ufildr  20167  alexsubALTlem3  20284  ptcmplem1  20287  restmetu  20825  ovolfiniun  21647  unmbl  21683  volfiniun  21692  voliunlem1  21695  plyun0  22329  lgsquadlem3  23359  axlowdimlem3  23923  axlowdimlem17  23937  usgrafilem1  24087  constr3trllem3  24328  constr3pthlem1  24331  ex-un  24822  ex-pw  24827  iuninc  27101  difico  27262  subfacp1lem1  28263  cvmliftlem10  28379  fprod2dlem  28687  wfrlem13  28932  wfrlem14  28933  wfrlem16  28935  mbfresfi  29638  asindmre  29679  mapfzcons  30252  mapfzcons1  30253  diophin  30310  iocunico  30783  fourierdlem65  31472  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem100  31507  fourierdlem105  31512  fourierdlem108  31515  fourierdlem109  31516  fourierdlem110  31517  fourierdlem112  31519  fourierdlem113  31520  lmod1zr  32175  bnj601  33057  bnj1416  33174  trclubg  36795
  Copyright terms: Public domain W3C validator