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

Theorem uneq2i 3640
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 3637 . 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 1383    u. cun 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466
This theorem is referenced by:  un4  3649  unundir  3651  difdif2  3740  difun2  3893  difdifdir  3901  dfif5  3942  qdass  4114  qdassr  4115  ssunpr  4177  iununi  4400  unidif0  4610  unisuc  4944  iunsuc  4950  difxp1  5422  fresaun  5746  fresaunres2  5747  fvssunirn  5879  fmptap  6079  fvsnun1  6091  funiunfv  6145  onuninsuci  6660  tfrlem10  7058  oarec  7213  dfdom2  7543  fodomr  7670  dfsup3OLD  7906  ranksuc  8286  kmlem3  8535  fin1a2lem10  8792  fin1a2lem12  8794  axdc3lem4  8836  prunioo  11660  facnn  12337  fac0  12338  hashun3  12434  fsum2dlem  13567  fsumiun  13617  incexclem  13630  fprod2dlem  13766  prmreclem4  14419  strlemor1  14706  strlemor2  14707  strlemor3  14708  phlstr  14760  mreexexlem4d  15026  opsrtoslem2  18128  restcld  19651  neitr  19659  fiuncmp  19882  refun0  19994  1stckgenlem  20032  filcon  20362  ufildr  20410  alexsubALTlem3  20527  ptcmplem1  20530  restmetu  21068  ovolfiniun  21890  unmbl  21926  volfiniun  21935  voliunlem1  21938  plyun0  22572  lgsquadlem3  23609  axlowdimlem3  24225  axlowdimlem17  24239  usgrafilem1  24389  constr3trllem3  24630  constr3pthlem1  24633  ex-un  25123  ex-pw  25128  iuninc  27406  difico  27572  subfacp1lem1  28601  cvmliftlem10  28717  wfrlem13  29331  wfrlem14  29332  wfrlem16  29334  mbfresfi  30037  asindmre  30078  mapfzcons  30624  mapfzcons1  30625  diophin  30682  iocunico  31154  fourierdlem65  31908  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem96  31939  fourierdlem97  31940  fourierdlem98  31941  fourierdlem99  31942  fourierdlem100  31943  fourierdlem105  31948  fourierdlem108  31951  fourierdlem109  31952  fourierdlem110  31953  fourierdlem112  31955  fourierdlem113  31956  lmod1zr  32964  bnj601  33846  bnj1416  33963  rp-fakeuninass  37579  trclubg  37613
  Copyright terms: Public domain W3C validator