Theorem eleq12d 2300

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  cbvraldva2  2772  cbvrexdva2  2773  cdeqel  3024  ru  3027  sbceqbid  3035  sbcel12g  3139  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  onintexmid  4662  elvvuni  4780  elrnmpt1  4971  canth  5945  smoeq  6426  smores  6428  smores2  6430  iordsmo  6433  nnaordi  6644  nnaordr  6646  fvixp  6840  cbvixp  6852  mptelixpg  6871  opabfi  7088  exmidaclem  7378  cc1  7439  cc2lem  7440  cc3  7442  ltapig  7513  ltmpig  7514  fzsubel  10244  elfzp1b  10281  wrd2ind  11241  ennnfonelemg  12960  ennnfonelemp1  12963  ennnfonelemnn0  12979  ctiunctlemu1st  12991  ctiunctlemu2nd  12992  ctiunctlemudc  12994  ctiunctlemfo  12996  prdsbasprj  13301  xpsfrnel  13363  ismgm  13376  mgm1  13389  issgrpd  13431  ismndd  13456  eqgfval  13745  ringcl  13962  unitinvcl  14072  aprval  14231  aprap  14235  islmodd  14242  rspcl  14440  rnglidlmmgm  14445  zndvds  14598  istps  14691  tpspropd  14695  eltpsg  14699  isms  15112  mspropd  15137  cnlimci  15332