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  4666  elvvuni  4785  elrnmpt1  4978  canth  5961  smoeq  6447  smores  6449  smores2  6451  iordsmo  6454  nnaordi  6667  nnaordr  6669  fvixp  6863  cbvixp  6875  mptelixpg  6894  opabfi  7116  exmidaclem  7406  cc1  7467  cc2lem  7468  cc3  7470  ltapig  7541  ltmpig  7542  fzsubel  10273  elfzp1b  10310  wrd2ind  11276  ennnfonelemg  12995  ennnfonelemp1  12998  ennnfonelemnn0  13014  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  ctiunctlemudc  13029  ctiunctlemfo  13031  prdsbasprj  13336  xpsfrnel  13398  ismgm  13411  mgm1  13424  issgrpd  13466  ismndd  13491  eqgfval  13780  ringcl  13997  unitinvcl  14108  aprval  14267  aprap  14271  islmodd  14278  rspcl  14476  rnglidlmmgm  14481  zndvds  14634  istps  14727  tpspropd  14731  eltpsg  14735  isms  15148  mspropd  15173  cnlimci  15368