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 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  cbvraldva2  2793  cbvrexdva2  2794  cdeqel  3047  ru  3050  sbceqbid  3058  sbcel12g  3162  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  onintexmid  4718  elvvuni  4837  elrnmpt1  5031  canth  6030  smoeq  6555  smores  6557  smores2  6559  iordsmo  6562  nnaordi  6775  nnaordr  6777  fvixp  6979  cbvixp  6991  mptelixpg  7010  opabfi  7241  exmidaclem  7558  cc1  7625  cc2lem  7626  cc3  7628  ltapig  7699  ltmpig  7700  fzsubel  10449  elfzp1b  10487  wrd2ind  11478  ennnfonelemg  13277  ennnfonelemp1  13280  ennnfonelemnn0  13296  ctiunctlemu1st  13308  ctiunctlemu2nd  13309  ctiunctlemudc  13311  ctiunctlemfo  13313  xpsfrnel  13648  ismgm  13660  mgm1  13673  issgrpd  13710  ismndd  13733  eqgfval  14008  prdsbasprj  14165  ringcl  14300  unitinvcl  14413  aprval  14574  aprap  14581  aprprop  14584  islmodd  14612  rspcl  14811  rnglidlmmgm  14816  zndvds  14967  istps  15116  tpspropd  15120  eltpsg  15124  isms  15537  mspropd  15562  cnlimci  15757  depindlem2  16731