Theorem eleq12d 2264

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  cbvraldva2  2733  cbvrexdva2  2734  cdeqel  2982  ru  2985  sbceqbid  2993  sbcel12g  3096  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  onintexmid  4606  elvvuni  4724  elrnmpt1  4914  canth  5872  smoeq  6345  smores  6347  smores2  6349  iordsmo  6352  nnaordi  6563  nnaordr  6565  fvixp  6759  cbvixp  6771  mptelixpg  6790  opabfi  6994  exmidaclem  7270  cc1  7327  cc2lem  7328  cc3  7330  ltapig  7400  ltmpig  7401  fzsubel  10129  elfzp1b  10166  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelemnn0  12582  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunctlemfo  12599  xpsfrnel  12930  ismgm  12943  mgm1  12956  issgrpd  12998  ismndd  13021  eqgfval  13295  ringcl  13512  unitinvcl  13622  aprval  13781  aprap  13785  islmodd  13792  rspcl  13990  rnglidlmmgm  13995  zndvds  14148  istps  14211  tpspropd  14215  eltpsg  14219  isms  14632  mspropd  14657  cnlimci  14852