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  4154  abssexg  4183  abnex  4448  snnex  4449  pwexb  4475  sucexb  4497  omex  4593  iprc  4896  dfse2  5002  fressnfv  5704  fnotovb  5918  f1stres  6160  f2ndres  6161  ottposg  6256  dftpos4  6264  frecabex  6399  oacl  6461  diffifi  6894  djuexb  7043  pitonn  7847  axicn  7862  pnfnre  7999  mnfnre  8000  0mnnnnn0  9208  nprmi  12124  issubm  12863  issrg  13148  srgfcl  13156  txdis1cn  13781  xmeterval  13938  expcncf  14095  bj-sucexg  14677