Theorem eleq12d 2309

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  cbvraldva2  2793  cbvrexdva2  2794  cdeqel  3047  ru  3050  sbceqbid  3058  sbcel12g  3162  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  onintexmid  4720  elvvuni  4839  elrnmpt1  5033  canth  6036  smoeq  6561  smores  6563  smores2  6565  iordsmo  6568  nnaordi  6781  nnaordr  6783  fvixp  6985  cbvixp  6997  mptelixpg  7016  opabfi  7247  exmidaclem  7564  cc1  7631  cc2lem  7632  cc3  7634  ltapig  7705  ltmpig  7706  fzsubel  10468  elfzp1b  10506  wrd2ind  11497  ennnfonelemg  13296  ennnfonelemp1  13299  ennnfonelemnn0  13315  ctiunctlemu1st  13327  ctiunctlemu2nd  13328  ctiunctlemudc  13330  ctiunctlemfo  13332  xpsfrnel  13667  ismgm  13679  mgm1  13692  issgrpd  13729  ismndd  13752  eqgfval  14027  prdsbasprj  14184  ringcl  14319  unitinvcl  14432  aprval  14593  aprap  14600  aprprop  14603  islmodd  14631  rspcl  14830  rnglidlmmgm  14835  zndvds  14986  istps  15135  tpspropd  15139  eltpsg  15143  isms  15556  mspropd  15581  cnlimci  15776  depindlem2  16760