Theorem eleq1i 2205

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

Syntax hints:   ↔ wb 104   = wceq 1331   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleq12i  2207  eqeltri  2212  intexrabim  4078  abssexg  4106  abnex  4368  snnex  4369  pwexb  4395  sucexb  4413  omex  4507  iprc  4807  dfse2  4912  fressnfv  5607  fnotovb  5814  f1stres  6057  f2ndres  6058  ottposg  6152  dftpos4  6160  frecabex  6295  oacl  6356  diffifi  6788  djuexb  6929  pitonn  7656  axicn  7671  pnfnre  7807  mnfnre  7808  0mnnnnn0  9009  nprmi  11805  txdis1cn  12447  xmeterval  12604  expcncf  12761  bj-sucexg  13120