Theorem eleq1a 2259

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

Syntax hints:   → wi 4   = wceq 1363   ∈ wcel 2158

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  elex22  2764  elex2  2765  reu6  2938  disjne  3488  ssimaex  5590  fnex  5751  f1ocnv2d  6089  mpoexw  6228  tfrlem8  6333  eroprf  6642  ac6sfi  6912  recclnq  7405  prnmaddl  7503  renegcl  8232  nn0ind-raph  9384  iccid  9939  4sqlem1  12400  4sqlem4  12404  lssvneln0  13562  lss1d  13572  lspsn  13605  rnglidlmmgm  13685  opnneiid  13960  metrest  14302  coseq0negpitopi  14553  bj-nn0suc  15012  bj-inf2vnlem2  15019  bj-nn0sucALT  15026