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  9595  fcdmnn0fsupp  9616  pfxccatin12lem3  11504  pfxccat3  11506  swrdccat  11507  pfxccat3a  11510  swrdccat3blem  11511  swrdccat3b  11512  nprmi  12902  issubm  13779  issrg  14269  srgfcl  14277  subrngrng  14510  txdis1cn  15379  xmeterval  15536  expcncf  15710  gausslemma2dlem1a  16177  2lgslem4  16222  clwwlknonex2  16680  bj-sucexg  16948