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

Theorem uneq1d 3619
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 3613 . 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 1437    u. cun 3434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441
This theorem is referenced by:  ifeq1  3915  preq1  4079  tpeq1  4088  tpeq2  4089  tpprceq3  4140  iununi  4387  resasplit  5770  fresaunres2  5772  fmptpr  6105  funresdfunsn  6122  ressuppssdif  6948  sbthlem5  7696  fodomr  7733  domunfican  7854  brwdom2  8098  cdaval  8608  ackbij1lem2  8659  ttukeylem3  8949  snunioo  11766  snunioc  11768  prunioo  11769  fzpred  11852  fseq1p1m1  11876  nn0split  11914  fzo0sn0fzo1  12008  fzosplitprm1  12025  s2prop  13000  s4prop  13001  fsum1p  13814  fprod1p  14022  setsval  15146  setsabs  15152  setscom  15153  prdsval  15353  prdsdsval  15376  prdsdsval2  15382  prdsdsval3  15383  mreexexlem3d  15552  mreexexlem4d  15553  estrres  16024  symg2bas  17039  evlseu  18739  ordtuni  20205  lfinun  20539  alexsubALTlem3  21063  ustssco  21228  trust  21243  ressprdsds  21385  xpsdsval  21395  nulmbl2  22489  uniioombllem3  22542  uniioombllem4  22543  plyeq0  23164  plyaddlem1  23166  plymullem1  23167  fta1lem  23259  vieta1lem2  23263  birthdaylem2  23877  nbgraopALT  25151  iunxdif3  28178  iuninc  28179  difelcarsg  29151  bnj1416  29857  mclsval  30210  mclsax  30216  rankung  30939  topjoin  31027  bj-tageq  31539  finixpnum  31895  poimirlem3  31908  poimirlem4  31909  poimirlem6  31911  poimirlem7  31912  poimirlem9  31914  poimirlem16  31921  poimirlem17  31922  poimirlem28  31933  mblfinlem2  31943  islshpsm  32516  lshpnel2N  32521  lkrlsp3  32640  pclfinclN  33485  dochsatshp  34989  mapfzcons1  35529  iunrelexp0  36265  fiiuncl  37380  nnsplit  37536  fourierdlem32  37943  fzopred  38590  fzopredsuc  38591  fzosplitpr  38920  aacllem  40191
  Copyright terms: Public domain W3C validator