Theorem eleq1i 2304

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

This proof depends on syntax axioms:   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12i  2306  eqeltri  2311  intexrabim  4291  abssexg  4321  abnex  4595  snnex  4596  pwexb  4622  sucexb  4646  omex  4742  iprc  5053  dfse2  5163  fressnfv  5905  fnotovb  6134  f1stres  6397  f2ndres  6398  ottposg  6531  dftpos4  6539  frecabex  6674  oacl  6738  diffifi  7204  djuexb  7390  pitonn  8221  axicn  8236  pnfnre  8373  mnfnre  8374  0mnnnnn0  9606  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  pfxccat3a  11531  swrdccat3blem  11532  swrdccat3b  11533  nprmi  12926  issubm  13837  issrg  14375  srgfcl  14383  subrngrng  14618  txdis1cn  15521  xmeterval  15678  expcncf  15852  ppi2i  16290  gausslemma2dlem1a  16399  2lgslem4  16444  clwwlknonex2  16902  bj-sucexg  17170