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

Theorem uneq2i 3504
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 3501 . 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 1364    u. cun 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3330
This theorem is referenced by:  un4  3513  unundir  3515  difdif2  3604  difun2  3755  difdifdir  3763  dfif5  3802  qdass  3971  qdassr  3972  ssunpr  4032  iununi  4252  unidif0  4462  unisuc  4791  iunsuc  4797  difxp1  5260  fresaun  5579  fresaunres2  5580  fvssunirn  5710  fmptap  5898  fvsnun1  5910  funiunfv  5962  onuninsuci  6450  tfrlem10  6842  oarec  6997  dfdom2  7331  fodomr  7458  dfsup3OLD  7690  ranksuc  8068  kmlem3  8317  fin1a2lem10  8574  fin1a2lem12  8576  axdc3lem4  8618  prunioo  11410  facnn  12049  fac0  12050  hashun3  12143  fsum2dlem  13233  fsumiun  13280  incexclem  13295  prmreclem4  13976  strlemor1  14261  strlemor2  14262  strlemor3  14263  phlstr  14315  mreexexlem4d  14581  opsrtoslem2  17542  restcld  18735  neitr  18743  fiuncmp  18966  1stckgenlem  19085  filcon  19415  ufildr  19463  alexsubALTlem3  19580  ptcmplem1  19583  restmetu  20121  ovolfiniun  20943  unmbl  20978  volfiniun  20987  voliunlem1  20990  plyun0  21624  lgsquadlem3  22654  axlowdimlem3  23125  axlowdimlem17  23139  usgrafilem1  23259  constr3trllem3  23473  constr3pthlem1  23476  ex-un  23566  ex-pw  23571  iuninc  25846  difico  26006  subfacp1lem1  26997  cvmliftlem10  27113  fprod2dlem  27420  wfrlem13  27665  wfrlem14  27666  wfrlem16  27668  mbfresfi  28363  asindmre  28404  mapfzcons  28977  mapfzcons1  28978  diophin  29036  iocunico  29511  lmod1zr  30876  bnj601  31747  bnj1416  31864
  Copyright terms: Public domain W3C validator