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

Theorem uneq12 3985
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 3983 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 3984 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2834 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  cun 3790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-un 3797
This theorem is referenced by:  uneq12i  3988  uneq12d  3991  un00  4237  opthprc  5415  dmpropg  5864  unixp  5924  fntpg  6196  fnun  6245  resasplit  6326  fvun  6530  rankprb  9013  pm54.43  9161  xpscg  16615  evlseu  19923  ptuncnv  22030  sshjval  28798  bj-2upleq  33580  poimirlem4  34048  poimirlem9  34053  diophun  38311  pwssplit4  38632  clsk1indlem3  39311
  Copyright terms: Public domain W3C validator