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  7932  axicn  7947  pnfnre  8085  mnfnre  8086  0mnnnnn0  9298  nprmi  12317  issubm  13174  issrg  13597  srgfcl  13605  subrngrng  13834  txdis1cn  14598  xmeterval  14755  expcncf  14929  gausslemma2dlem1a  15383  2lgslem4  15428  bj-sucexg  15652