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

Theorem uneq2 3722
Description: Equality theorem for the union of two classes. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
uneq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem uneq2
StepHypRef Expression
1 uneq1 3721 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uncom 3718 . 2 (𝐶𝐴) = (𝐴𝐶)
3 uncom 3718 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2668 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544
This theorem is referenced by:  uneq12  3723  uneq2i  3725  uneq2d  3728  uneqin  3836  disjssun  3987  uniprg  4380  unexb  6833  undifixp  7807  unxpdom  8029  ackbij1lem16  8917  fin23lem28  9022  ttukeylem6  9196  lcmfun  15142  ipodrsima  16934  mplsubglem  19201  mretopd  20648  iscldtop  20651  dfcon2  20974  nconsubb  20978  comppfsc  21087  spanun  27594  locfinref  29042  isros  29364  unelros  29367  difelros  29368  rossros  29376  inelcarsg  29506  nofulllem1  30907  rankung  31249  paddval  33898  dochsatshp  35554  nacsfix  36089  eldioph4b  36189  eldioph4i  36190  fiuneneq  36590  isotone1  37162  fiiuncl  38055
  Copyright terms: Public domain W3C validator