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

Theorem uneq12 4158
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 4156 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 4157 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2793 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  cun 3946
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 3953
This theorem is referenced by:  uneq12i  4161  uneq12d  4164  un00  4442  opthprc  5739  dmpropg  6212  unixp  6279  fntpg  6606  fnun  6661  resasplit  6759  fvun  6979  rankprb  9843  pm54.43  9993  pwmndgplus  18813  evlseu  21638  ptuncnv  23303  sshjval  30591  bj-2upleq  35882  bj-unexg  35908  poimirlem4  36481  poimirlem9  36486  evlselvlem  41156  diophun  41497  pwssplit4  41817  clsk1indlem3  42780
  Copyright terms: Public domain W3C validator