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  7385  pitonn  8216  axicn  8231  pnfnre  8368  mnfnre  8369  0mnnnnn0  9600  fcdmnn0fsupp  9621  pfxccatin12lem3  11520  pfxccat3  11522  swrdccat  11523  pfxccat3a  11526  swrdccat3blem  11527  swrdccat3b  11528  nprmi  12921  issubm  13832  issrg  14353  srgfcl  14361  subrngrng  14594  txdis1cn  15470  xmeterval  15627  expcncf  15801  ppi2i  16234  gausslemma2dlem1a  16343  2lgslem4  16388  clwwlknonex2  16846  bj-sucexg  17114