Theorem eleq1i 2178

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

Syntax hints:   ↔ wb 104   = wceq 1312   ∈ wcel 1461

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109

This theorem is referenced by:  eleq12i  2180  eqeltri  2185  intexrabim  4036  abssexg  4064  abnex  4326  snnex  4327  pwexb  4353  sucexb  4371  omex  4465  iprc  4763  dfse2  4868  fressnfv  5559  fnotovb  5766  f1stres  6008  f2ndres  6009  ottposg  6103  dftpos4  6111  frecabex  6246  oacl  6307  diffifi  6738  djuexb  6878  pitonn  7576  axicn  7591  pnfnre  7724  mnfnre  7725  0mnnnnn0  8906  nprmi  11644  txdis1cn  12282  xmeterval  12417  expcncf  12571  bj-sucexg  12799