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

Theorem uneq2 3298
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 3297 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3294 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3294 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2315 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    u. cun 3125
This theorem is referenced by:  uneq12  3299  uneq2i  3301  uneq2d  3304  uneqin  3395  disjssun  3487  uniprg  3816  sucprc  4439  unexb  4492  undifixp  6820  unxpdom  7038  ackbij1lem16  7829  fin23lem28  7934  ttukeylem6  8109  ipodrsima  14231  mplsubglem  16142  mretopd  16792  iscldtop  16795  dfcon2  17108  nconsubb  17112  spanun  22085  axfelem9  23724  brsuccf  23856  rankung  24172  domfldref  24428  repfuntw  24528  comppfsc  25675  nacsfix  26155  eldioph4b  26262  eldioph4i  26263  fiuneneq  26881  paddval  29237  dochsatshp  30891
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132
  Copyright terms: Public domain W3C validator