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

Theorem uneq2 3284
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 3283 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3280 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3280 . 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 3111
This theorem is referenced by:  uneq12  3285  uneq2i  3287  uneq2d  3290  uneqin  3381  disjssun  3473  uniprg  3802  sucprc  4425  unexb  4478  undifixp  6806  unxpdom  7024  ackbij1lem16  7815  fin23lem28  7920  ttukeylem6  8095  ipodrsima  14216  mplsubglem  16127  mretopd  16777  iscldtop  16780  dfcon2  17093  nconsubb  17097  spanun  22070  axfelem9  23709  brsuccf  23841  rankung  24157  domfldref  24413  repfuntw  24513  comppfsc  25660  nacsfix  26140  eldioph4b  26247  eldioph4i  26248  fiuneneq  26866  paddval  29138  dochsatshp  30792
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 2759  df-un 3118
  Copyright terms: Public domain W3C validator