Theorem eleq12d 2241

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 2240	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2239	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 187	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  cbvraldva2  2703  cbvrexdva2  2704  cdeqel  2951  ru  2954  sbcel12g  3064  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  onintexmid  4555  elvvuni  4673  elrnmpt1  4860  canth  5804  smoeq  6266  smores  6268  smores2  6270  iordsmo  6273  nnaordi  6484  nnaordr  6486  fvixp  6677  cbvixp  6689  mptelixpg  6708  exmidaclem  7172  cc1  7214  cc2lem  7215  cc3  7217  ltapig  7287  ltmpig  7288  fzsubel  10003  elfzp1b  10040  ennnfonelemg  12345  ennnfonelemp1  12348  ennnfonelemnn0  12364  ctiunctlemu1st  12376  ctiunctlemu2nd  12377  ctiunctlemudc  12379  ctiunctlemfo  12381  ismgm  12598  mgm1  12611  ismndd  12660  istps  12783  tpspropd  12787  eltpsg  12791  isms  13206  mspropd  13231  cnlimci  13395