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

Theorem uneq1i 3494
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 3491 . 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 1362    u. cun 3314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321
This theorem is referenced by:  un12  3502  unundi  3505  undif1  3742  dfif5  3793  tpcoma  3959  qdass  3962  qdassr  3963  tpidm12  3964  unidif0  4453  difxp2  5252  resasplit  5569  fresaun  5570  fresaunres2  5571  fmptpr  5890  df2o3  6921  sbthlem6  7414  fodomr  7450  domss2  7458  domunfican  7572  kmlem11  8317  hashfun  12183  prmreclem2  13961  setscom  14187  uniioombllem3  20907  lhop  21330  usgrafilem1  23147  constr3pthlem1  23364  ex-un  23454  ex-pw  23459  subfacp1lem1  26915  dftrpred4g  27545  symdifV  27703  lineunray  28025  lmod1  30743  bnj1415  31731  bj-2upln1upl  32100
  Copyright terms: Public domain W3C validator