Theorem eleq1i 2259

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq1i	⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Proof of Theorem eleq1i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq1 2256	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1364   ∈ wcel 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleq12i  2261  eqeltri  2266  intexrabim  4182  abssexg  4211  abnex  4478  snnex  4479  pwexb  4505  sucexb  4529  omex  4625  iprc  4930  dfse2  5038  fressnfv  5745  fnotovb  5961  f1stres  6212  f2ndres  6213  ottposg  6308  dftpos4  6316  frecabex  6451  oacl  6513  diffifi  6950  djuexb  7103  pitonn  7908  axicn  7923  pnfnre  8061  mnfnre  8062  0mnnnnn0  9272  nprmi  12262  issubm  13044  issrg  13461  srgfcl  13469  subrngrng  13698  txdis1cn  14446  xmeterval  14603  expcncf  14763  gausslemma2dlem1a  15174  bj-sucexg  15414