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  4289  abssexg  4319  abnex  4593  snnex  4594  pwexb  4620  sucexb  4644  omex  4740  iprc  5051  dfse2  5160  fressnfv  5902  fnotovb  6131  f1stres  6393  f2ndres  6394  ottposg  6526  dftpos4  6534  frecabex  6669  oacl  6733  diffifi  7198  djuexb  7384  pitonn  8215  axicn  8230  pnfnre  8367  mnfnre  8368  0mnnnnn0  9599  fcdmnn0fsupp  9620  pfxccatin12lem3  11518  pfxccat3  11520  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  nprmi  12918  issubm  13828  issrg  14318  srgfcl  14326  subrngrng  14559  txdis1cn  15428  xmeterval  15585  expcncf  15759  ppi2i  16178  gausslemma2dlem1a  16275  2lgslem4  16320  clwwlknonex2  16778  bj-sucexg  17046