Theorem eleq12d 2305

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  cbvraldva2  2787  cbvrexdva2  2788  cdeqel  3041  ru  3044  sbceqbid  3052  sbcel12g  3156  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  onintexmid  4700  elvvuni  4819  elrnmpt1  5013  canth  6009  smoeq  6534  smores  6536  smores2  6538  iordsmo  6541  nnaordi  6754  nnaordr  6756  fvixp  6951  cbvixp  6963  mptelixpg  6982  opabfi  7213  exmidaclem  7528  cc1  7595  cc2lem  7596  cc3  7598  ltapig  7669  ltmpig  7670  fzsubel  10418  elfzp1b  10456  wrd2ind  11443  ennnfonelemg  13242  ennnfonelemp1  13245  ennnfonelemnn0  13261  ctiunctlemu1st  13273  ctiunctlemu2nd  13274  ctiunctlemudc  13276  ctiunctlemfo  13278  xpsfrnel  13612  ismgm  13624  mgm1  13637  issgrpd  13679  ismndd  13702  eqgfval  13979  prdsbasprj  14128  ringcl  14260  unitinvcl  14372  aprval  14533  aprap  14540  aprprop  14543  islmodd  14571  rspcl  14769  rnglidlmmgm  14774  zndvds  14927  istps  15027  tpspropd  15031  eltpsg  15035  isms  15448  mspropd  15473  cnlimci  15668  depindlem2  16632