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

Theorem uneq1d 3341
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 3335 . 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 1632    u. cun 3163
This theorem is referenced by:  ifeq1  3582  preq1  3719  tpeq1  3728  tpeq2  3729  iununi  4002  resasplit  5427  fresaunres2  5429  sbthlem5  6991  fodomr  7028  domunfican  7145  brwdom2  7303  cdaval  7812  ackbij1lem2  7863  ttukeylem3  8154  snunioo  10778  prunioo  10780  fseq1p1m1  10873  elfzp12  10877  fsum1p  12234  setsval  13188  setsabs  13191  setscom  13192  prdsval  13371  prdsdsval  13393  prdsdsval2  13399  prdsdsval3  13400  mreexexlem3d  13564  mreexexlem4d  13565  ordtuni  16936  alexsubALTlem3  17759  ressprdsds  17951  xpsdsval  17961  nulmbl2  18910  uniioombllem3  18956  uniioombllem4  18957  evlseu  19416  plyeq0  19609  plyaddlem1  19611  plymullem1  19612  fta1lem  19703  vieta1lem2  19707  birthdaylem2  20263  iuninc  23174  fmptpr  23229  snunioc  23282  rankung  24868  topjoin  26417  mapfzcons1  26897  tpprceq3  28182  s2prop  28221  s4prop  28222  bnj1416  29385  islshpsm  29792  lshpnel2N  29797  lkrlsp3  29916  pclfinclN  30761  dochsatshp  32263
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170
  Copyright terms: Public domain W3C validator