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

Theorem uneq2 3323
Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
uneq2  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )

Proof of Theorem uneq2
StepHypRef Expression
1 uneq1 3322 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3319 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3319 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2340 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150
This theorem is referenced by:  uneq12  3324  uneq2i  3326  uneq2d  3329  uneqin  3420  disjssun  3512  uniprg  3842  sucprc  4467  unexb  4520  undifixp  6852  unxpdom  7070  ackbij1lem16  7861  fin23lem28  7966  ttukeylem6  8141  ipodrsima  14268  mplsubglem  16179  mretopd  16829  iscldtop  16832  dfcon2  17145  nconsubb  17149  spanun  22124  nofulllem1  23767  brsuccf  23891  rankung  24207  domfldref  24473  repfuntw  24572  comppfsc  25719  nacsfix  26199  eldioph4b  26306  eldioph4i  26307  fiuneneq  26925  paddval  29360  dochsatshp  31014
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator