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

Theorem uneq12 4159
Description: Equality theorem for the union of two classes. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
uneq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem uneq12
StepHypRef Expression
1 uneq1 4157 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 4158 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2793 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  cun 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954
This theorem is referenced by:  uneq12i  4162  uneq12d  4165  un00  4443  opthprc  5741  dmpropg  6215  unixp  6282  fntpg  6609  fnun  6664  resasplit  6762  fvun  6982  rankprb  9846  pm54.43  9996  pwmndgplus  18816  evlseu  21646  ptuncnv  23311  sshjval  30603  bj-2upleq  35893  bj-unexg  35919  poimirlem4  36492  poimirlem9  36497  evlselvlem  41158  diophun  41511  pwssplit4  41831  clsk1indlem3  42794
  Copyright terms: Public domain W3C validator