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  3025  ru  3028  sbceqbid  3036  sbcel12g  3140  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  onintexmid  4669  elvvuni  4788  elrnmpt1  4981  canth  5964  smoeq  6451  smores  6453  smores2  6455  iordsmo  6458  nnaordi  6671  nnaordr  6673  fvixp  6867  cbvixp  6879  mptelixpg  6898  opabfi  7126  exmidaclem  7416  cc1  7477  cc2lem  7478  cc3  7480  ltapig  7551  ltmpig  7552  fzsubel  10288  elfzp1b  10325  wrd2ind  11297  ennnfonelemg  13017  ennnfonelemp1  13020  ennnfonelemnn0  13036  ctiunctlemu1st  13048  ctiunctlemu2nd  13049  ctiunctlemudc  13051  ctiunctlemfo  13053  prdsbasprj  13358  xpsfrnel  13420  ismgm  13433  mgm1  13446  issgrpd  13488  ismndd  13513  eqgfval  13802  ringcl  14019  unitinvcl  14130  aprval  14289  aprap  14293  islmodd  14300  rspcl  14498  rnglidlmmgm  14503  zndvds  14656  istps  14749  tpspropd  14753  eltpsg  14757  isms  15170  mspropd  15195  cnlimci  15390