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

Theorem uneq12 3723
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 3721 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 3722 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2663 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = 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 2032  ax-13 2232  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:  uneq12i  3726  uneq12d  3729  un00  3962  opthprc  5079  dmpropg  5512  unixp  5571  fntpg  5848  fnun  5897  resasplit  5972  fvun  6163  rankprb  8574  pm54.43  8686  xpscg  15987  evlseu  19283  ptuncnv  21362  sshjval  27399  bj-2upleq  31996  poimirlem4  32386  poimirlem9  32391  diophun  36158  pwssplit4  36480  clsk1indlem3  37164
  Copyright terms: Public domain W3C validator