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

Theorem uneq2 3912
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 3911 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uncom 3908 . 2 (𝐶𝐴) = (𝐴𝐶)
3 uncom 3908 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2830 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cun 3721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728
This theorem is referenced by:  uneq12  3913  uneq2i  3915  uneq2d  3918  uneqin  4027  disjssun  4178  uniprg  4588  unexb  7105  undifixp  8098  unxpdom  8323  ackbij1lem16  9259  fin23lem28  9364  ttukeylem6  9538  lcmfun  15566  ipodrsima  17373  mplsubglem  19649  mretopd  21117  iscldtop  21120  dfconn2  21443  nconnsubb  21447  comppfsc  21556  spanun  28744  locfinref  30248  isros  30571  unelros  30574  difelros  30575  rossros  30583  inelcarsg  30713  noextendseq  32157  rankung  32610  paddval  35606  dochsatshp  37261  nacsfix  37801  eldioph4b  37901  eldioph4i  37902  fiuneneq  38301  isotone1  38872  fiiuncl  39755
  Copyright terms: Public domain W3C validator