Theorem eleq12d 2303

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  cbvraldva2  2784  cbvrexdva2  2785  cdeqel  3037  ru  3040  sbceqbid  3048  sbcel12g  3152  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  onintexmid  4694  elvvuni  4813  elrnmpt1  5007  canth  6000  smoeq  6520  smores  6522  smores2  6524  iordsmo  6527  nnaordi  6740  nnaordr  6742  fvixp  6937  cbvixp  6949  mptelixpg  6968  opabfi  7199  exmidaclem  7514  cc1  7578  cc2lem  7579  cc3  7581  ltapig  7652  ltmpig  7653  fzsubel  10393  elfzp1b  10430  wrd2ind  11411  ennnfonelemg  13146  ennnfonelemp1  13149  ennnfonelemnn0  13165  ctiunctlemu1st  13177  ctiunctlemu2nd  13178  ctiunctlemudc  13180  ctiunctlemfo  13182  prdsbasprj  13487  xpsfrnel  13549  ismgm  13562  mgm1  13575  issgrpd  13617  ismndd  13642  eqgfval  13931  ringcl  14149  unitinvcl  14260  aprval  14420  aprap  14424  islmodd  14433  rspcl  14631  rnglidlmmgm  14636  zndvds  14789  istps  14889  tpspropd  14893  eltpsg  14897  isms  15310  mspropd  15335  cnlimci  15530  depindlem2  16494