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

Theorem uneq1d 3653
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 3647 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  u.  C
)  =  ( B  u.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    u. cun 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476
This theorem is referenced by:  ifeq1  3948  preq1  4111  tpeq1  4120  tpeq2  4121  tpprceq3  4172  iununi  4420  resasplit  5761  fresaunres2  5763  fmptpr  6097  funresdfunsn  6114  ressuppssdif  6939  sbthlem5  7650  fodomr  7687  domunfican  7811  brwdom2  8017  cdaval  8567  ackbij1lem2  8618  ttukeylem3  8908  snunioo  11671  snunioc  11673  prunioo  11674  fzpred  11753  fseq1p1m1  11777  nn0split  11815  fzo0sn0fzo1  11904  fzosplitprm1  11921  s2prop  12873  s4prop  12874  fsum1p  13579  fprod1p  13783  setsval  14668  setsabs  14674  setscom  14675  prdsval  14871  prdsdsval  14894  prdsdsval2  14900  prdsdsval3  14901  mreexexlem3d  15062  mreexexlem4d  15063  estrres  15534  symg2bas  16549  evlseu  18311  ordtuni  19817  lfinun  20151  alexsubALTlem3  20674  ustssco  20842  trust  20857  ressprdsds  20999  xpsdsval  21009  nulmbl2  22072  uniioombllem3  22119  uniioombllem4  22120  plyeq0  22733  plyaddlem1  22735  plymullem1  22736  fta1lem  22828  vieta1lem2  22832  birthdaylem2  23407  nbgraopALT  24550  iunxdif3  27564  iuninc  27565  difelcarsg  28440  mclsval  29098  mclsax  29104  rankung  29985  finixpnum  30200  mblfinlem2  30214  topjoin  30345  mapfzcons1  30811  fourierdlem32  32082  fzosplitpr  32564  aacllem  33318  bnj1416  34196  bj-tageq  34635  islshpsm  34806  lshpnel2N  34811  lkrlsp3  34930  pclfinclN  35775  dochsatshp  37279
  Copyright terms: Public domain W3C validator