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

Theorem uneq2i 3569
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 3566 . 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 1399    u. cun 3387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394
This theorem is referenced by:  un4  3578  unundir  3580  difdif2  3680  difun2  3823  difdifdir  3831  dfif5  3873  qdass  4043  qdassr  4044  ssunpr  4106  iununi  4331  unidif0  4538  unisuc  4868  iunsuc  4874  difxp1  5342  fresaun  5664  fresaunres2  5665  fvssunirn  5797  fmptap  5996  fvsnun1  6008  funiunfv  6061  onuninsuci  6574  tfrlem10  6974  oarec  7129  dfdom2  7460  fodomr  7587  ranksuc  8196  kmlem3  8445  fin1a2lem10  8702  fin1a2lem12  8704  axdc3lem4  8746  prunioo  11570  facnn  12257  fac0  12258  hashun3  12355  trclublem  12833  dmtrclfv  12856  fsum2dlem  13587  fsumiun  13637  incexclem  13650  fprod2dlem  13786  prmreclem4  14439  strlemor1  14729  strlemor2  14730  strlemor3  14731  phlstr  14787  mreexexlem4d  15054  opsrtoslem2  18262  restcld  19759  neitr  19767  fiuncmp  19990  refun0  20101  1stckgenlem  20139  filcon  20469  ufildr  20517  alexsubALTlem3  20634  ptcmplem1  20637  restmetu  21175  ovolfiniun  21997  unmbl  22033  volfiniun  22042  voliunlem1  22045  plyun0  22679  lgsquadlem3  23748  axlowdimlem3  24368  axlowdimlem17  24382  usgrafilem1  24532  constr3trllem3  24773  constr3pthlem1  24776  ex-un  25266  ex-pw  25271  indifundif  27535  iuninc  27557  difico  27747  esum2dlem  28240  fiunelcarsg  28443  carsgclctunlem1  28444  carsggect  28445  subfacp1lem1  28812  cvmliftlem10  28928  wfrlem13  29520  wfrlem14  29521  wfrlem16  29523  mbfresfi  30226  asindmre  30268  mapfzcons  30814  mapfzcons1  30815  diophin  30871  iocunico  31346  fourierdlem65  32120  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem96  32151  fourierdlem97  32152  fourierdlem98  32153  fourierdlem99  32154  fourierdlem100  32155  fourierdlem105  32160  fourierdlem108  32163  fourierdlem109  32164  fourierdlem110  32165  fourierdlem112  32167  fourierdlem113  32168  lmod1zr  33294  bnj601  34325  bnj1416  34442  rp-fakeuninass  38171  dfrcl2  38211  corcltrcl  38249  cotrclrcl  38250
  Copyright terms: Public domain W3C validator