Theorem eleq1a 2278

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  elex22  2789  elex2  2790  reu6  2966  disjne  3518  ssimaex  5652  fnex  5818  f1ocnv2d  6162  mpoexw  6311  tfrlem8  6416  eroprf  6727  ac6sfi  7009  recclnq  7520  prnmaddl  7618  mpomulf  8077  renegcl  8348  nn0ind-raph  9505  iccid  10062  4sqlem1  12781  4sqlem4  12785  4sqlem11  12794  lssvneln0  14205  lss1d  14215  lspsn  14248  rnglidlmmgm  14328  opnneiid  14706  metrest  15048  coseq0negpitopi  15378  bj-nn0suc  16034  bj-inf2vnlem2  16041  bj-nn0sucALT  16048