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

Theorem uneq2 3324
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 3323 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3320 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3320 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2341 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3151
This theorem is referenced by:  uneq12  3325  uneq2i  3327  uneq2d  3330  uneqin  3421  disjssun  3513  uniprg  3843  sucprc  4466  unexb  4519  undifixp  6848  unxpdom  7066  ackbij1lem16  7857  fin23lem28  7962  ttukeylem6  8137  ipodrsima  14264  mplsubglem  16175  mretopd  16825  iscldtop  16828  dfcon2  17141  nconsubb  17145  spanun  22120  axfelem9  23758  brsuccf  23890  rankung  24206  domfldref  24471  repfuntw  24571  comppfsc  25718  nacsfix  26198  eldioph4b  26305  eldioph4i  26306  fiuneneq  26924  paddval  29266  dochsatshp  30920
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158
  Copyright terms: Public domain W3C validator