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

Theorem uneq1d 3507
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 3501 . 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 1369    u. cun 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3331
This theorem is referenced by:  ifeq1  3793  preq1  3952  tpeq1  3961  tpeq2  3962  tpprceq3  4011  iununi  4253  resasplit  5579  fresaunres2  5581  fmptpr  5901  funresdfunsn  5918  ressuppssdif  6708  sbthlem5  7423  fodomr  7460  domunfican  7582  brwdom2  7786  cdaval  8337  ackbij1lem2  8388  ttukeylem3  8678  snunioo  11409  snunioc  11411  prunioo  11412  fzpred  11501  fseq1p1m1  11532  elfzp12  11537  fzo0sn0fzo1  11615  s2prop  12522  s4prop  12523  fsum1p  13220  setsval  14196  setsabs  14201  setscom  14202  prdsval  14391  prdsdsval  14414  prdsdsval2  14420  prdsdsval3  14421  mreexexlem3d  14582  mreexexlem4d  14583  symg2bas  15901  evlseu  17600  ordtuni  18792  alexsubALTlem3  19619  ustssco  19787  trust  19802  ressprdsds  19944  xpsdsval  19954  nulmbl2  21016  uniioombllem3  21063  uniioombllem4  21064  plyeq0  21677  plyaddlem1  21679  plymullem1  21680  fta1lem  21771  vieta1lem2  21775  birthdaylem2  22344  iuninc  25909  fprod1p  27476  rankung  28202  finixpnum  28411  mblfinlem2  28426  topjoin  28583  mapfzcons1  29050  fzosplitpr  30220  fzosplitprm1  30221  bnj1416  32027  bj-tageq  32466  islshpsm  32622  lshpnel2N  32627  lkrlsp3  32746  pclfinclN  33591  dochsatshp  35093
  Copyright terms: Public domain W3C validator