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

Theorem uneq1i 3617
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 3614 . 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 1370    u. cun 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444
This theorem is referenced by:  un12  3625  unundi  3628  undif1  3865  dfif5  3916  tpcoma  4082  qdass  4085  qdassr  4086  tpidm12  4087  unidif0  4576  difxp2  5375  resasplit  5692  fresaun  5693  fresaunres2  5694  fmptpr  6015  df2o3  7046  sbthlem6  7539  fodomr  7575  domss2  7583  domunfican  7698  kmlem11  8444  hashfun  12321  prmreclem2  14100  setscom  14326  gsummptfzsplitl  16552  uniioombllem3  21208  lhop  21631  usgrafilem1  23503  constr3pthlem1  23720  ex-un  23810  ex-pw  23815  subfacp1lem1  27234  dftrpred4g  27865  symdifV  28023  lineunray  28345  lmod1  31189  bnj1415  32384  bj-2upln1upl  32874
  Copyright terms: Public domain W3C validator