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

Theorem uneq2 3265
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 3264 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3261 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3261 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2313 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    u. cun 3092
This theorem is referenced by:  uneq12  3266  uneq2i  3268  uneq2d  3271  uneqin  3362  disjssun  3454  uniprg  3783  sucprc  4404  unexb  4457  undifixp  6785  unxpdom  7003  ackbij1lem16  7794  fin23lem28  7899  ttukeylem6  8074  ipodrsima  14195  mplsubglem  16106  mretopd  16756  iscldtop  16759  dfcon2  17072  nconsubb  17076  spanun  22049  axfelem9  23688  brsuccf  23820  rankung  24136  domfldref  24392  repfuntw  24492  comppfsc  25639  nacsfix  26119  eldioph4b  26226  eldioph4i  26227  fiuneneq  26845  paddval  29117  dochsatshp  30771
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-un 3099
  Copyright terms: Public domain W3C validator