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

Theorem uneq1i 3659
Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1  |-  A  =  B
Assertion
Ref Expression
uneq1i  |-  ( A  u.  C )  =  ( B  u.  C
)

Proof of Theorem uneq1i
StepHypRef Expression
1 uneq1i.1 . 2  |-  A  =  B
2 uneq1 3656 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 5 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    u. cun 3479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-un 3486
This theorem is referenced by:  un12  3667  unundi  3670  undif1  3907  dfif5  3960  tpcoma  4128  qdass  4131  qdassr  4132  tpidm12  4133  unidif0  4625  difxp2  5438  resasplit  5760  fresaun  5761  fresaunres2  5762  fmptpr  6096  df2o3  7153  sbthlem6  7642  fodomr  7678  domss2  7686  domunfican  7803  kmlem11  8550  hashfun  12471  prmreclem2  14306  setscom  14532  gsummptfzsplitl  16803  uniioombllem3  21839  lhop  22262  usgrafilem1  24202  constr3pthlem1  24446  ex-un  24937  ex-pw  24942  subfacp1lem1  28416  dftrpred4g  29212  symdifV  29370  lineunray  29692  fourierdlem80  31778  usgfislem1  32202  usgfisALTlem1  32206  lmod1  32467  bnj1415  33466  bj-2upln1upl  33956
  Copyright terms: Public domain W3C validator