Theorem eleq1i 2236

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

Syntax hints:   ↔ wb 104   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12i  2238  eqeltri  2243  intexrabim  4139  abssexg  4168  abnex  4432  snnex  4433  pwexb  4459  sucexb  4481  omex  4577  iprc  4879  dfse2  4984  fressnfv  5683  fnotovb  5896  f1stres  6138  f2ndres  6139  ottposg  6234  dftpos4  6242  frecabex  6377  oacl  6439  diffifi  6872  djuexb  7021  pitonn  7810  axicn  7825  pnfnre  7961  mnfnre  7962  0mnnnnn0  9167  nprmi  12078  issubm  12695  txdis1cn  13072  xmeterval  13229  expcncf  13386  bj-sucexg  13957