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

Theorem uneq12 3754
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 3752 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 uneq2 3753 . 2 (𝐶 = 𝐷 → (𝐵𝐶) = (𝐵𝐷))
31, 2sylan9eq 2674 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  cun 3565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572
This theorem is referenced by:  uneq12i  3757  uneq12d  3760  un00  4002  opthprc  5157  dmpropg  5596  unixp  5656  fntpg  5936  fnun  5985  resasplit  6061  fvun  6255  rankprb  8699  pm54.43  8811  xpscg  16199  evlseu  19497  ptuncnv  21591  sshjval  28179  bj-2upleq  32975  poimirlem4  33384  poimirlem9  33389  diophun  37156  pwssplit4  37478  clsk1indlem3  38161
  Copyright terms: Public domain W3C validator