Theorem eleq12d 2302

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  cbvraldva2  2775  cbvrexdva2  2776  cdeqel  3028  ru  3031  sbceqbid  3039  sbcel12g  3143  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  onintexmid  4677  elvvuni  4796  elrnmpt1  4989  canth  5979  smoeq  6499  smores  6501  smores2  6503  iordsmo  6506  nnaordi  6719  nnaordr  6721  fvixp  6915  cbvixp  6927  mptelixpg  6946  opabfi  7175  exmidaclem  7466  cc1  7527  cc2lem  7528  cc3  7530  ltapig  7601  ltmpig  7602  fzsubel  10338  elfzp1b  10375  wrd2ind  11351  ennnfonelemg  13085  ennnfonelemp1  13088  ennnfonelemnn0  13104  ctiunctlemu1st  13116  ctiunctlemu2nd  13117  ctiunctlemudc  13119  ctiunctlemfo  13121  prdsbasprj  13426  xpsfrnel  13488  ismgm  13501  mgm1  13514  issgrpd  13556  ismndd  13581  eqgfval  13870  ringcl  14088  unitinvcl  14199  aprval  14358  aprap  14362  islmodd  14369  rspcl  14567  rnglidlmmgm  14572  zndvds  14725  istps  14823  tpspropd  14827  eltpsg  14831  isms  15244  mspropd  15269  cnlimci  15464  depindlem2  16428