Theorem eleq1i 2150

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

Syntax hints:   ↔ wb 103   = wceq 1287   ∈ wcel 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081

This theorem is referenced by:  eleq12i  2152  eqeltri  2157  intexrabim  3964  abssexg  3991  snnex  4245  pwexb  4270  sucexb  4287  omex  4381  iprc  4669  dfse2  4772  fressnfv  5447  fnotovb  5649  f1stres  5887  f2ndres  5888  ottposg  5974  dftpos4  5982  frecabex  6117  oacl  6175  diffifi  6562  pitonn  7329  axicn  7344  pnfnre  7473  mnfnre  7474  0mnnnnn0  8638  nprmi  10981  bj-sucexg  11251