Theorem eleq1a 2277

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 2268	. 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 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  elex22  2787  elex2  2788  reu6  2962  disjne  3514  ssimaex  5640  fnex  5806  f1ocnv2d  6150  mpoexw  6299  tfrlem8  6404  eroprf  6715  ac6sfi  6995  recclnq  7505  prnmaddl  7603  mpomulf  8062  renegcl  8333  nn0ind-raph  9490  iccid  10047  4sqlem1  12711  4sqlem4  12715  4sqlem11  12724  lssvneln0  14135  lss1d  14145  lspsn  14178  rnglidlmmgm  14258  opnneiid  14636  metrest  14978  coseq0negpitopi  15308  bj-nn0suc  15900  bj-inf2vnlem2  15907  bj-nn0sucALT  15914