Theorem eleq1i 2243

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

Syntax hints:   ↔ wb 105   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12i  2245  eqeltri  2250  intexrabim  4153  abssexg  4182  abnex  4447  snnex  4448  pwexb  4474  sucexb  4496  omex  4592  iprc  4895  dfse2  5001  fressnfv  5703  fnotovb  5917  f1stres  6159  f2ndres  6160  ottposg  6255  dftpos4  6263  frecabex  6398  oacl  6460  diffifi  6893  djuexb  7042  pitonn  7846  axicn  7861  pnfnre  7998  mnfnre  7999  0mnnnnn0  9207  nprmi  12123  issubm  12862  issrg  13146  srgfcl  13154  txdis1cn  13748  xmeterval  13905  expcncf  14062  bj-sucexg  14644