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

Theorem uneq1i 3401
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 3398 . 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 1642    u. cun 3226
This theorem is referenced by:  un12  3409  unundi  3412  undif1  3605  dfif5  3653  tpcoma  3799  qdass  3802  qdassr  3803  tpidm12  3804  unidif0  4262  resasplit  5491  fresaun  5492  fresaunres2  5493  difxp2  6239  df2o3  6576  sbthlem6  7061  fodomr  7097  domss2  7105  domunfican  7216  kmlem11  7873  hashfun  11479  prmreclem2  13055  setscom  13267  uniioombllem3  19038  lhop  19461  ex-un  20917  ex-pw  20922  fmptpr  23262  subfacp1lem1  24114  dftrpred4g  24795  symdifV  24927  lineunray  25329  usgrafilem1  27571  cusgrasizeindslem1  27628  constr3pthlem1  27762  bnj1415  28813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-un 3233
  Copyright terms: Public domain W3C validator