Theorem eleq12d 2237

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)

Hypotheses

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eleq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eleq12d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Proof of Theorem eleq12d

Step	Hyp	Ref	Expression
1		eleq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	eleq2d 2236	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2235	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  cbvraldva2  2699  cbvrexdva2  2700  cdeqel  2947  ru  2950  sbcel12g  3060  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  onintexmid  4550  elvvuni  4668  elrnmpt1  4855  canth  5796  smoeq  6258  smores  6260  smores2  6262  iordsmo  6265  nnaordi  6476  nnaordr  6478  fvixp  6669  cbvixp  6681  mptelixpg  6700  exmidaclem  7164  cc1  7206  cc2lem  7207  cc3  7209  ltapig  7279  ltmpig  7280  fzsubel  9995  elfzp1b  10032  ennnfonelemg  12336  ennnfonelemp1  12339  ennnfonelemnn0  12355  ctiunctlemu1st  12367  ctiunctlemu2nd  12368  ctiunctlemudc  12370  ctiunctlemfo  12372  ismgm  12588  mgm1  12601  istps  12670  tpspropd  12674  eltpsg  12678  isms  13093  mspropd  13118  cnlimci  13282