Theorem eleq1a 2109

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 2100	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 149	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1243   ∈ wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  elex22  2569  elex2  2570  reu6  2730  disjne  3273  ssimaex  5234  fnex  5383  f1ocnv2d  5704  tfrlem8  5934  eroprf  6199  ac6sfi  6352  recclnq  6490  prnmaddl  6588  renegcl  7272  nn0ind-raph  8355  iccid  8794  bj-nn0suc  10089  bj-inf2vnlem2  10096  bj-nn0sucALT  10103