Theorem eleq1a 2310

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
eleq1a	⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 2301	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 160	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  elex22  2837  elex2  2838  reu6  3015  disjne  3578  ssimaex  5764  fnex  5937  f1ocnv2d  6294  f1o3d  6298  mpoexw  6449  tfrlem8  6589  eroprf  6902  ac6sfi  7202  recclnq  7759  prnmaddl  7857  mpomulf  8316  renegcl  8588  nn0ind-raph  9767  iccid  10337  4sqlem1  13187  4sqlem4  13191  4sqlem11  13200  lssvneln0  14759  lss1d  14769  lspsn  14802  rnglidlmmgm  14882  opnneiid  15314  metrest  15656  coseq0negpitopi  15987  ppiublem1  16192  bj-nn0suc  17088  bj-inf2vnlem2  17095  bj-nn0sucALT  17102