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

Theorem uneq2i 3587
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 3584 . 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 1446    u. cun 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-un 3411
This theorem is referenced by:  un4  3596  unundir  3598  difdif2  3702  difun2  3849  difdifdir  3857  dfif5  3899  qdass  4074  qdassr  4075  ssunpr  4137  iununi  4369  unidif0  4579  difxp1  5265  unisuc  5502  iunsuc  5508  fresaun  5759  fresaunres2  5760  fvssunirn  5893  fmptap  6092  fvsnun1  6104  funiunfv  6158  onuninsuci  6672  wfrlem13  7053  wfrlem14  7054  wfrlem16  7056  tfrlem10  7110  oarec  7268  dfdom2  7600  fodomr  7728  ranksuc  8341  kmlem3  8587  fin1a2lem10  8844  fin1a2lem12  8846  axdc3lem4  8888  prunioo  11768  facnn  12468  fac0  12469  hashun3  12570  trclublem  13071  dmtrclfv  13094  fsum2dlem  13843  fsumiun  13893  incexclem  13906  fprod2dlem  14046  prmreclem4  14875  strlemor1  15229  strlemor2  15230  strlemor3  15231  phlstr  15290  mreexexlem4d  15565  opsrtoslem2  18720  restcld  20200  neitr  20208  fiuncmp  20431  refun0  20542  1stckgenlem  20580  filcon  20910  ufildr  20958  alexsubALTlem3  21076  ptcmplem1  21079  restmetu  21597  ovolfiniun  22466  unmbl  22503  volfiniun  22512  voliunlem1  22515  plyun0  23163  lgsquadlem3  24296  axlowdimlem3  24986  axlowdimlem17  25000  usgrafilem1  25151  constr3trllem3  25392  constr3pthlem1  25395  ex-un  25886  ex-pw  25891  indifundif  28164  iuninc  28188  difico  28377  esum2dlem  28925  fiunelcarsg  29160  carsgclctunlem1  29161  carsggect  29162  bnj601  29743  bnj1416  29860  subfacp1lem1  29914  cvmliftlem10  30029  poimirlem4  31956  poimirlem18  31970  poimirlem21  31973  poimirlem22  31974  poimirlem25  31977  mbfresfi  31999  asindmre  32039  mapfzcons  35570  mapfzcons1  35571  diophin  35627  iocunico  36107  rp-fakeuninass  36173  rclexi  36234  rtrclex  36236  dfrtrcl5  36248  dfrcl2  36278  corcltrcl  36343  cotrclrcl  36346  frege109d  36361  frege131d  36368  fiiuncl  37416  fourierdlem65  38045  fourierdlem89  38069  fourierdlem90  38070  fourierdlem91  38071  fourierdlem96  38076  fourierdlem97  38077  fourierdlem98  38078  fourierdlem99  38079  fourierdlem100  38080  fourierdlem105  38085  fourierdlem108  38088  fourierdlem109  38089  fourierdlem110  38090  fourierdlem112  38092  fourierdlem113  38093  isomenndlem  38361  hoidmvlelem3  38429  1fzopredsuc  38731  lmod1zr  40390
  Copyright terms: Public domain W3C validator