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

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

Proof of Theorem eleq12
StepHypRef Expression
1 eleq1 2718 . 2 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
2 eleq2 2719 . 2 (𝐶 = 𝐷 → (𝐵𝐶𝐵𝐷))
31, 2sylan9bb 736 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  trel  4792  pwnss  4860  epelg  5059  preleq  8552  oemapval  8618  cantnf  8628  wemapwe  8632  nnsdomel  8854  cldval  20875  isufil  21754  umgr2v2enb1  26478  issiga  30302  matunitlindf  33537  wepwsolem  37929  aomclem8  37948  nelbr  41615
  Copyright terms: Public domain W3C validator