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

Theorem uneq2 4136
 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 4135 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uncom 4132 . 2 (𝐶𝐴) = (𝐴𝐶)
3 uncom 4132 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2884 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1536   ∪ cun 3937 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944 This theorem is referenced by:  uneq12  4137  uneq2i  4139  uneq2d  4142  uneqin  4258  disjssun  4420  uniprg  4859  unexb  7474  undifixp  8501  unxpdom  8728  ackbij1lem16  9660  fin23lem28  9765  ttukeylem6  9939  lcmfun  15992  ipodrsima  17778  mplsubglem  20217  mretopd  21703  iscldtop  21706  dfconn2  22030  nconnsubb  22034  comppfsc  22143  spanun  29325  locfinref  31109  isros  31431  unelros  31434  difelros  31435  rossros  31443  inelcarsg  31573  noextendseq  33178  rankung  33631  bj-funun  34538  paddval  36938  dochsatshp  38591  nacsfix  39315  eldioph4b  39414  eldioph4i  39415  fiuneneq  39803  isotone1  40404  fiiuncl  41333
 Copyright terms: Public domain W3C validator