Theorem eleq1i 2272

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

Syntax hints:   ↔ wb 105   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12i  2274  eqeltri  2279  intexrabim  4205  abssexg  4234  abnex  4502  snnex  4503  pwexb  4529  sucexb  4553  omex  4649  iprc  4956  dfse2  5064  fressnfv  5784  fnotovb  6001  f1stres  6258  f2ndres  6259  ottposg  6354  dftpos4  6362  frecabex  6497  oacl  6559  diffifi  7006  djuexb  7161  pitonn  7981  axicn  7996  pnfnre  8134  mnfnre  8135  0mnnnnn0  9347  nprmi  12521  issubm  13379  issrg  13802  srgfcl  13810  subrngrng  14039  txdis1cn  14825  xmeterval  14982  expcncf  15156  gausslemma2dlem1a  15610  2lgslem4  15655  bj-sucexg  15996