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

Theorem eleq12 2793
 Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)
Assertion
Ref Expression
eleq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))

Proof of Theorem eleq12
StepHypRef Expression
1 eleq1 2791 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 eleq2 2792 . 2 (𝐶 = 𝐷 → (𝐵𝐶𝐵𝐷))
31, 2sylan9bb 738 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1596   ∈ wcel 2103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-ext 2704 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1818  df-cleq 2717  df-clel 2720 This theorem is referenced by:  trel  4867  pwnss  4935  epelg  5134  preleq  8627  oemapval  8693  cantnf  8703  wemapwe  8707  nnsdomel  8929  cldval  20950  isufil  21829  umgr2v2enb1  26553  issiga  30404  matunitlindf  33639  wepwsolem  38031  aomclem8  38050  nelbr  41717
 Copyright terms: Public domain W3C validator