Theorem eleq1i 2241

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 2238	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2146

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  eleq12i  2243  eqeltri  2248  intexrabim  4148  abssexg  4177  abnex  4441  snnex  4442  pwexb  4468  sucexb  4490  omex  4586  iprc  4888  dfse2  4994  fressnfv  5695  fnotovb  5908  f1stres  6150  f2ndres  6151  ottposg  6246  dftpos4  6254  frecabex  6389  oacl  6451  diffifi  6884  djuexb  7033  pitonn  7822  axicn  7837  pnfnre  7973  mnfnre  7974  0mnnnnn0  9181  nprmi  12091  issubm  12735  issrg  12954  srgfcl  12962  txdis1cn  13358  xmeterval  13515  expcncf  13672  bj-sucexg  14243