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

Theorem uneq12 3628
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 3626 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 3627 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2568 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  cun 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079  df-un 3449
This theorem is referenced by:  uneq12i  3631  uneq12d  3634  un00  3866  opthprc  4983  dmpropg  5416  unixp  5475  fntpg  5752  fnun  5801  resasplit  5876  fvun  6067  rankprb  8477  pm54.43  8589  xpscg  15937  evlseu  19245  ptuncnv  21327  sshjval  27385  bj-2upleq  32028  poimirlem4  32477  poimirlem9  32482  diophun  36249  pwssplit4  36571  clsk1indlem3  37262
  Copyright terms: Public domain W3C validator