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

Theorem uneq2 3615
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 3614 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
2 uncom 3611 . 2  |-  ( C  u.  A )  =  ( A  u.  C
)
3 uncom 3611 . 2  |-  ( C  u.  B )  =  ( B  u.  C
)
41, 2, 33eqtr4g 2520 1  |-  ( A  =  B  ->  ( C  u.  A )  =  ( C  u.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    u. cun 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444
This theorem is referenced by:  uneq12  3616  uneq2i  3618  uneq2d  3621  uneqin  3712  disjssun  3847  uniprg  4216  sucprc  4905  unexb  6493  undifixp  7412  unxpdom  7634  ackbij1lem16  8518  fin23lem28  8623  ttukeylem6  8797  ipodrsima  15457  mplsubglem  17637  mplsubglemOLD  17639  mretopd  18831  iscldtop  18834  dfcon2  19158  nconsubb  19162  spanun  25120  nofulllem1  28007  brsuccf  28136  rankung  28368  comppfsc  28747  nacsfix  29216  eldioph4b  29318  eldioph4i  29319  fiuneneq  29730  paddval  33800  dochsatshp  35454
  Copyright terms: Public domain W3C validator