Theorem eleq1i 2232

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

Syntax hints:   ↔ wb 104   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12i  2234  eqeltri  2239  intexrabim  4132  abssexg  4161  abnex  4425  snnex  4426  pwexb  4452  sucexb  4474  omex  4570  iprc  4872  dfse2  4977  fressnfv  5672  fnotovb  5885  f1stres  6127  f2ndres  6128  ottposg  6223  dftpos4  6231  frecabex  6366  oacl  6428  diffifi  6860  djuexb  7009  pitonn  7789  axicn  7804  pnfnre  7940  mnfnre  7941  0mnnnnn0  9146  nprmi  12056  txdis1cn  12928  xmeterval  13085  expcncf  13242  bj-sucexg  13814