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  7565  cc1  7632  cc2lem  7633  cc3  7635  ltapig  7706  ltmpig  7707  fzsubel  10477  elfzp1b  10515  wrd2ind  11511  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelemnn0  13365  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  xpsfrnel  13717  ismgm  13729  mgm1  13742  issgrpd  13779  ismndd  13802  eqgfval  14077  prdsbasprj  14234  ringcl  14369  unitinvcl  14482  aprval  14643  aprap  14650  aprprop  14653  islmodd  14681  rspcl  14880  rnglidlmmgm  14885  zndvds  15036  istps  15192  tpspropd  15196  eltpsg  15200  isms  15613  mspropd  15638  cnlimci  15833  depindlem2  16882