Theorem eleq1i 2262

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleq12i  2264  eqeltri  2269  intexrabim  4187  abssexg  4216  abnex  4483  snnex  4484  pwexb  4510  sucexb  4534  omex  4630  iprc  4935  dfse2  5043  fressnfv  5752  fnotovb  5969  f1stres  6226  f2ndres  6227  ottposg  6322  dftpos4  6330  frecabex  6465  oacl  6527  diffifi  6964  djuexb  7119  pitonn  7934  axicn  7949  pnfnre  8087  mnfnre  8088  0mnnnnn0  9300  nprmi  12319  issubm  13176  issrg  13599  srgfcl  13607  subrngrng  13836  txdis1cn  14622  xmeterval  14779  expcncf  14953  gausslemma2dlem1a  15407  2lgslem4  15452  bj-sucexg  15676