Theorem eleq1a 2268

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  elex22  2778  elex2  2779  reu6  2953  disjne  3504  ssimaex  5622  fnex  5784  f1ocnv2d  6127  mpoexw  6271  tfrlem8  6376  eroprf  6687  ac6sfi  6959  recclnq  7459  prnmaddl  7557  mpomulf  8016  renegcl  8287  nn0ind-raph  9443  iccid  10000  4sqlem1  12557  4sqlem4  12561  4sqlem11  12570  lssvneln0  13929  lss1d  13939  lspsn  13972  rnglidlmmgm  14052  opnneiid  14400  metrest  14742  coseq0negpitopi  15072  bj-nn0suc  15610  bj-inf2vnlem2  15617  bj-nn0sucALT  15624