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

Theorem uneq1d 3657
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 3651 . 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 1379    u. cun 3474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481
This theorem is referenced by:  ifeq1  3943  preq1  4106  tpeq1  4115  tpeq2  4116  tpprceq3  4167  iununi  4410  resasplit  5755  fresaunres2  5757  fmptpr  6086  funresdfunsn  6103  ressuppssdif  6921  sbthlem5  7631  fodomr  7668  domunfican  7793  brwdom2  7999  cdaval  8550  ackbij1lem2  8601  ttukeylem3  8891  snunioo  11646  snunioc  11648  prunioo  11649  fzpred  11728  fseq1p1m1  11752  elfzp12  11757  nn0split  11787  fzo0sn0fzo1  11870  fzosplitprm1  11887  s2prop  12825  s4prop  12826  fsum1p  13531  setsval  14514  setsabs  14519  setscom  14520  prdsval  14710  prdsdsval  14733  prdsdsval2  14739  prdsdsval3  14740  mreexexlem3d  14901  mreexexlem4d  14902  symg2bas  16228  evlseu  17984  ordtuni  19485  alexsubALTlem3  20312  ustssco  20480  trust  20495  ressprdsds  20637  xpsdsval  20647  nulmbl2  21710  uniioombllem3  21757  uniioombllem4  21758  plyeq0  22371  plyaddlem1  22373  plymullem1  22374  fta1lem  22465  vieta1lem2  22469  birthdaylem2  23038  nbgraopALT  24128  iuninc  27129  fprod1p  28702  rankung  29428  finixpnum  29643  mblfinlem2  29657  topjoin  29814  mapfzcons1  30281  fourierdlem32  31467  fzosplitpr  31837  bnj1416  33192  bj-tageq  33633  islshpsm  33795  lshpnel2N  33800  lkrlsp3  33919  pclfinclN  34764  dochsatshp  36266
  Copyright terms: Public domain W3C validator