Theorem eleq12d 2248

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  cbvraldva2  2712  cbvrexdva2  2713  cdeqel  2960  ru  2963  sbceqbid  2971  sbcel12g  3074  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  onintexmid  4574  elvvuni  4692  elrnmpt1  4880  canth  5831  smoeq  6293  smores  6295  smores2  6297  iordsmo  6300  nnaordi  6511  nnaordr  6513  fvixp  6705  cbvixp  6717  mptelixpg  6736  exmidaclem  7209  cc1  7266  cc2lem  7267  cc3  7269  ltapig  7339  ltmpig  7340  fzsubel  10062  elfzp1b  10099  ennnfonelemg  12406  ennnfonelemp1  12409  ennnfonelemnn0  12425  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  xpsfrnel  12768  ismgm  12781  mgm1  12794  ismndd  12843  eqgfval  13086  ringcl  13201  unitinvcl  13297  aprval  13377  aprap  13381  islmodd  13388  istps  13571  tpspropd  13575  eltpsg  13579  isms  13992  mspropd  14017  cnlimci  14181