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

Theorem uneq1d 3599
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 3593 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2syl 17 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    u. cun 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421
This theorem is referenced by:  ifeq1  3897  preq1  4064  tpeq1  4073  tpeq2  4074  tpprceq3  4125  iunxdif3  4378  iununi  4382  resasplit  5780  fresaunres2  5782  fmptpr  6118  funresdfunsn  6135  ressuppssdif  6968  sbthlem5  7717  fodomr  7754  domunfican  7875  brwdom2  8119  cdaval  8631  ackbij1lem2  8682  ttukeylem3  8972  snunioo  11793  snunioc  11795  prunioo  11796  fzpred  11879  fseq1p1m1  11903  nn0split  11942  fzo0sn0fzo1  12038  fzosplitprm1  12055  s2prop  13044  s4prop  13047  fsum1p  13869  fprod1p  14077  setsval  15201  setsabs  15207  setscom  15208  prdsval  15408  prdsdsval  15431  prdsdsval2  15437  prdsdsval3  15438  mreexexlem3d  15607  mreexexlem4d  15608  estrres  16079  symg2bas  17094  evlseu  18794  ordtuni  20261  lfinun  20595  alexsubALTlem3  21119  ustssco  21284  trust  21299  ressprdsds  21441  xpsdsval  21451  nulmbl2  22545  uniioombllem3  22599  uniioombllem4  22600  plyeq0  23221  plyaddlem1  23223  plymullem1  23224  fta1lem  23316  vieta1lem2  23320  birthdaylem2  23934  nbgraopALT  25208  iuninc  28230  difelcarsg  29192  bnj1416  29898  mclsval  30251  mclsax  30257  rankung  30983  topjoin  31071  bj-tageq  31616  finixpnum  31976  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem9  31995  poimirlem16  32002  poimirlem17  32003  poimirlem28  32014  mblfinlem2  32024  islshpsm  32592  lshpnel2N  32597  lkrlsp3  32716  pclfinclN  33561  dochsatshp  35065  mapfzcons1  35605  iunrelexp0  36340  fiiuncl  37445  nnsplit  37656  fourierdlem32  38103  fzopred  38854  fzopredsuc  38855  fzosplitpr  39203  aacllem  40909
  Copyright terms: Public domain W3C validator