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

Theorem uneq1d 3500
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 3494 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3318
This theorem is referenced by:  ifeq1  3743  preq1  3883  tpeq1  3892  tpeq2  3893  tpprceq3  3938  iununi  4175  resasplit  5613  fresaunres2  5615  sbthlem5  7221  fodomr  7258  domunfican  7379  brwdom2  7541  cdaval  8050  ackbij1lem2  8101  ttukeylem3  8391  snunioo  11023  prunioo  11025  fseq1p1m1  11122  elfzp12  11126  s2prop  11861  s4prop  11862  fsum1p  12539  setsval  13493  setsabs  13496  setscom  13497  prdsval  13678  prdsdsval  13700  prdsdsval2  13706  prdsdsval3  13707  mreexexlem3d  13871  mreexexlem4d  13872  ordtuni  17254  alexsubALTlem3  18080  ustssco  18244  trust  18259  ressprdsds  18401  xpsdsval  18411  nulmbl2  19431  uniioombllem3  19477  uniioombllem4  19478  evlseu  19937  plyeq0  20130  plyaddlem1  20132  plymullem1  20133  fta1lem  20224  vieta1lem2  20228  birthdaylem2  20791  iuninc  24011  fmptpr  24062  snunioc  24137  fprod1p  25291  rankung  26107  mblfinlem2  26244  topjoin  26394  mapfzcons1  26773  fzo0sn0fzo1  28125  bnj1416  29408  islshpsm  29778  lshpnel2N  29783  lkrlsp3  29902  pclfinclN  30747  dochsatshp  32249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325
  Copyright terms: Public domain W3C validator