Theorem eleq12d 2267

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  cbvraldva2  2736  cbvrexdva2  2737  cdeqel  2985  ru  2988  sbceqbid  2996  sbcel12g  3099  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  onintexmid  4610  elvvuni  4728  elrnmpt1  4918  canth  5878  smoeq  6357  smores  6359  smores2  6361  iordsmo  6364  nnaordi  6575  nnaordr  6577  fvixp  6771  cbvixp  6783  mptelixpg  6802  opabfi  7008  exmidaclem  7291  cc1  7348  cc2lem  7349  cc3  7351  ltapig  7422  ltmpig  7423  fzsubel  10152  elfzp1b  10189  ennnfonelemg  12645  ennnfonelemp1  12648  ennnfonelemnn0  12664  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunctlemfo  12681  prdsbasprj  12984  xpsfrnel  13046  ismgm  13059  mgm1  13072  issgrpd  13114  ismndd  13139  eqgfval  13428  ringcl  13645  unitinvcl  13755  aprval  13914  aprap  13918  islmodd  13925  rspcl  14123  rnglidlmmgm  14128  zndvds  14281  istps  14352  tpspropd  14356  eltpsg  14360  isms  14773  mspropd  14798  cnlimci  14993