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  4557  elvvuni  4675  elrnmpt1  4862  canth  5807  smoeq  6269  smores  6271  smores2  6273  iordsmo  6276  nnaordi  6487  nnaordr  6489  fvixp  6681  cbvixp  6693  mptelixpg  6712  exmidaclem  7185  cc1  7227  cc2lem  7228  cc3  7230  ltapig  7300  ltmpig  7301  fzsubel  10016  elfzp1b  10053  ennnfonelemg  12358  ennnfonelemp1  12361  ennnfonelemnn0  12377  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394  ismgm  12611  mgm1  12624  ismndd  12673  istps  12824  tpspropd  12828  eltpsg  12832  isms  13247  mspropd  13272  cnlimci  13436