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

Theorem uneq1i 3499
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 3496 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 5 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1653    u. cun 3320
This theorem is referenced by:  un12  3507  unundi  3510  undif1  3705  dfif5  3753  tpcoma  3902  qdass  3905  qdassr  3906  tpidm12  3907  unidif0  4375  resasplit  5616  fresaun  5617  fresaunres2  5618  difxp2  6385  df2o3  6740  sbthlem6  7225  fodomr  7261  domss2  7269  domunfican  7382  kmlem11  8045  hashfun  11705  prmreclem2  13290  setscom  13502  uniioombllem3  19482  lhop  19905  usgrafilem1  21430  constr3pthlem1  21647  ex-un  21737  ex-pw  21742  fmptpr  24067  subfacp1lem1  24870  dftrpred4g  25517  symdifV  25675  lineunray  26086  bnj1415  29481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327
  Copyright terms: Public domain W3C validator