Theorem eleq12 2793

Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.)

Assertion

Ref	Expression
eleq12	⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Proof of Theorem eleq12

Step	Hyp	Ref	Expression
1		eleq1 2791	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
2		eleq2 2792	. 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))
3	1, 2	sylan9bb 738	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

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