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

Theorem uneq1d 3328
Description: Deduction adding union to the right in a class equality. (Contributed by NM, 29-Mar-1998.)
Hypothesis
Ref Expression
uneq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
uneq1d  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  C ) )

Proof of Theorem uneq1d
StepHypRef Expression
1 uneq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 uneq1 3322 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2syl 15 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150
This theorem is referenced by:  ifeq1  3569  preq1  3706  tpeq1  3715  tpeq2  3716  iununi  3986  resasplit  5411  fresaunres2  5413  sbthlem5  6975  fodomr  7012  domunfican  7129  brwdom2  7287  cdaval  7796  ackbij1lem2  7847  ttukeylem3  8138  snunioo  10762  prunioo  10764  fseq1p1m1  10857  elfzp12  10861  fsum1p  12218  setsval  13172  setsabs  13175  setscom  13176  prdsval  13355  prdsdsval  13377  prdsdsval2  13383  prdsdsval3  13384  mreexexlem3d  13548  mreexexlem4d  13549  ordtuni  16920  alexsubALTlem3  17743  ressprdsds  17935  xpsdsval  17945  nulmbl2  18894  uniioombllem3  18940  uniioombllem4  18941  evlseu  19400  plyeq0  19593  plyaddlem1  19595  plymullem1  19596  fta1lem  19687  vieta1lem2  19691  birthdaylem2  20247  iuninc  23158  fmptpr  23214  snunioc  23267  rankung  24796  topjoin  26314  mapfzcons1  26794  tpprceq3  28072  s2prop  28089  s4prop  28090  bnj1416  29069  islshpsm  29170  lshpnel2N  29175  lkrlsp3  29294  pclfinclN  30139  dochsatshp  31641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator