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

Theorem uneq2 3325
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 3324 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3321 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3321 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2342 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    u. cun 3152
This theorem is referenced by:  uneq12  3326  uneq2i  3328  uneq2d  3331  uneqin  3422  disjssun  3514  uniprg  3844  sucprc  4469  unexb  4522  undifixp  6854  unxpdom  7072  ackbij1lem16  7863  fin23lem28  7968  ttukeylem6  8143  ipodrsima  14270  mplsubglem  16181  mretopd  16831  iscldtop  16834  dfcon2  17147  nconsubb  17151  spanun  22126  nofulllem1  24358  brsuccf  24482  rankung  24798  domfldref  25072  comppfsc  26318  nacsfix  26798  eldioph4b  26905  eldioph4i  26906  fiuneneq  27524  paddval  30060  dochsatshp  31714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159
  Copyright terms: Public domain W3C validator