Theorem eleq1i 2270

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

Syntax hints:   ↔ wb 105   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eleq12i  2272  eqeltri  2277  intexrabim  4196  abssexg  4225  abnex  4492  snnex  4493  pwexb  4519  sucexb  4543  omex  4639  iprc  4944  dfse2  5052  fressnfv  5761  fnotovb  5978  f1stres  6235  f2ndres  6236  ottposg  6331  dftpos4  6339  frecabex  6474  oacl  6536  diffifi  6973  djuexb  7128  pitonn  7943  axicn  7958  pnfnre  8096  mnfnre  8097  0mnnnnn0  9309  nprmi  12365  issubm  13222  issrg  13645  srgfcl  13653  subrngrng  13882  txdis1cn  14668  xmeterval  14825  expcncf  14999  gausslemma2dlem1a  15453  2lgslem4  15498  bj-sucexg  15722