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

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

Proof of Theorem eleq12
StepHypRef Expression
1 eleq1 2676 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 eleq2 2677 . 2 (𝐶 = 𝐷 → (𝐵𝐶𝐵𝐷))
31, 2sylan9bb 732 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  trel  4682  pwnss  4751  epelg  4940  preleq  8375  oemapval  8441  cantnf  8451  wemapwe  8455  nnsdomel  8677  cldval  20585  isufil  21465  issiga  29295  matunitlindf  32371  wepwsolem  36424  aomclem8  36443  umgr2v2enb1  40734
  Copyright terms: Public domain W3C validator