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 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  elex22  2837  elex2  2838  reu6  3015  disjne  3577  ssimaex  5758  fnex  5928  f1ocnv2d  6284  f1o3d  6288  mpoexw  6439  tfrlem8  6579  eroprf  6892  ac6sfi  7192  recclnq  7749  prnmaddl  7847  mpomulf  8306  renegcl  8577  nn0ind-raph  9742  iccid  10306  4sqlem1  13145  4sqlem4  13149  4sqlem11  13158  lssvneln0  14682  lss1d  14692  lspsn  14725  rnglidlmmgm  14805  opnneiid  15188  metrest  15530  coseq0negpitopi  15860  bj-nn0suc  16904  bj-inf2vnlem2  16911  bj-nn0sucALT  16918