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

Theorem uneq1i 3465
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 3462 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 8 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1649    u. cun 3286
This theorem is referenced by:  un12  3473  unundi  3476  undif1  3671  dfif5  3719  tpcoma  3868  qdass  3871  qdassr  3872  tpidm12  3873  unidif0  4340  resasplit  5580  fresaun  5581  fresaunres2  5582  difxp2  6349  df2o3  6704  sbthlem6  7189  fodomr  7225  domss2  7233  domunfican  7346  kmlem11  8004  hashfun  11663  prmreclem2  13248  setscom  13460  uniioombllem3  19438  lhop  19861  usgrafilem1  21386  constr3pthlem1  21603  ex-un  21693  ex-pw  21698  fmptpr  24023  subfacp1lem1  24826  dftrpred4g  25459  symdifV  25591  lineunray  25993  bnj1415  29125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293
  Copyright terms: Public domain W3C validator