Theorem eleq1a 2279

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
eleq1a	|- ( A e. B -> ( C = A -> C e. B ) )

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 2270	. 2 |- ( C = A -> ( C e. B <-> A e. B ) )
2	1	biimprcd 160	1 |- ( A e. B -> ( C = A -> C e. B ) )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2178

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 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  elex22  2792  elex2  2793  reu6  2969  disjne  3522  ssimaex  5663  fnex  5829  f1ocnv2d  6173  mpoexw  6322  tfrlem8  6427  eroprf  6738  ac6sfi  7021  recclnq  7540  prnmaddl  7638  mpomulf  8097  renegcl  8368  nn0ind-raph  9525  iccid  10082  4sqlem1  12826  4sqlem4  12830  4sqlem11  12839  lssvneln0  14250  lss1d  14260  lspsn  14293  rnglidlmmgm  14373  opnneiid  14751  metrest  15093  coseq0negpitopi  15423  bj-nn0suc  16099  bj-inf2vnlem2  16106  bj-nn0sucALT  16113