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

Theorem uneq2 3583
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 3582 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3579 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3579 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2462 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    u. cun 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-v 3053  df-un 3411
This theorem is referenced by:  uneq12  3584  uneq2i  3586  uneq2d  3589  uneqin  3691  disjssun  3817  uniprg  4194  sucprc  4884  unexb  6521  undifixp  7446  unxpdom  7665  ackbij1lem16  8550  fin23lem28  8655  ttukeylem6  8829  ipodrsima  15935  mplsubglem  18229  mplsubglemOLD  18231  mretopd  19702  iscldtop  19705  dfcon2  20028  nconsubb  20032  comppfsc  20141  spanun  26605  locfinref  28033  inelcarsg  28478  nofulllem1  29667  brsuccf  29784  rankung  30016  nacsfix  30850  eldioph4b  30950  eldioph4i  30951  fiuneneq  31362  paddval  35974  dochsatshp  37630
  Copyright terms: Public domain W3C validator