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  2710  cbvrexdva2  2711  cdeqel  2958  ru  2961  sbceqbid  2969  sbcel12g  3072  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  onintexmid  4570  elvvuni  4688  elrnmpt1  4875  canth  5824  smoeq  6286  smores  6288  smores2  6290  iordsmo  6293  nnaordi  6504  nnaordr  6506  fvixp  6698  cbvixp  6710  mptelixpg  6729  exmidaclem  7202  cc1  7259  cc2lem  7260  cc3  7262  ltapig  7332  ltmpig  7333  fzsubel  10053  elfzp1b  10090  ennnfonelemg  12394  ennnfonelemp1  12397  ennnfonelemnn0  12413  ctiunctlemu1st  12425  ctiunctlemu2nd  12426  ctiunctlemudc  12428  ctiunctlemfo  12430  ismgm  12706  mgm1  12719  ismndd  12768  ringcl  13096  unitinvcl  13191  aprval  13239  aprap  13243  istps  13312  tpspropd  13316  eltpsg  13320  isms  13735  mspropd  13760  cnlimci  13924