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

Theorem uneq2i 3576
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 3573 . 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 1452    u. cun 3388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395
This theorem is referenced by:  un4  3585  unundir  3587  difdif2  3691  difun2  3838  difdifdir  3846  dfif5  3888  qdass  4062  qdassr  4063  ssunpr  4126  iununi  4359  unidif0  4574  difxp1  5268  unisuc  5506  iunsuc  5512  fresaun  5766  fresaunres2  5767  fvssunirn  5902  fmptap  6103  fvsnun1  6115  funiunfv  6171  onuninsuci  6686  wfrlem13  7066  wfrlem14  7067  wfrlem16  7069  tfrlem10  7123  oarec  7281  dfdom2  7613  fodomr  7741  ranksuc  8354  kmlem3  8600  fin1a2lem10  8857  fin1a2lem12  8859  axdc3lem4  8901  prunioo  11787  fz0sn0fz1  11933  facnn  12499  fac0  12500  hashun3  12601  trclublem  13134  dmtrclfv  13159  fsum2dlem  13908  fsumiun  13958  incexclem  13971  fprod2dlem  14111  prmreclem4  14942  strlemor1  15295  strlemor2  15296  strlemor3  15297  phlstr  15356  mreexexlem4d  15631  opsrtoslem2  18785  restcld  20265  neitr  20273  fiuncmp  20496  refun0  20607  1stckgenlem  20645  filcon  20976  ufildr  21024  alexsubALTlem3  21142  ptcmplem1  21145  restmetu  21663  ovolfiniun  22532  unmbl  22569  volfiniun  22579  voliunlem1  22582  plyun0  23230  lgsquadlem3  24363  axlowdimlem3  25053  axlowdimlem17  25067  usgrafilem1  25218  constr3trllem3  25459  constr3pthlem1  25462  ex-un  25953  ex-pw  25958  indifundif  28231  iuninc  28253  difico  28440  esum2dlem  28987  fiunelcarsg  29221  carsgclctunlem1  29222  carsggect  29223  bnj601  29803  bnj1416  29920  subfacp1lem1  29974  cvmliftlem10  30089  poimirlem4  32008  poimirlem18  32022  poimirlem21  32025  poimirlem22  32026  poimirlem25  32029  mbfresfi  32051  asindmre  32091  mapfzcons  35629  mapfzcons1  35630  diophin  35686  iocunico  36166  rp-fakeuninass  36232  rclexi  36293  rtrclex  36295  dfrtrcl5  36307  dfrcl2  36337  corcltrcl  36402  cotrclrcl  36405  frege109d  36420  frege131d  36427  fiiuncl  37465  fourierdlem65  38147  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  fourierdlem96  38178  fourierdlem97  38179  fourierdlem98  38180  fourierdlem99  38181  fourierdlem100  38182  fourierdlem105  38187  fourierdlem108  38190  fourierdlem109  38191  fourierdlem110  38192  fourierdlem112  38194  fourierdlem113  38195  isomenndlem  38470  hoidmvlelem3  38537  1fzopredsuc  38866  lmod1zr  40794
  Copyright terms: Public domain W3C validator