Theorem eleq1a 1543

Description: A transitive-type law relating membership and equality.

Assertion

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

Proof of Theorem eleq1a

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

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958

This theorem is referenced by:  reu3 1931  uniiunlem 2132  prss 2471  tpss 2476  ordtr2 3002  peano5 3153  ssimaex 3768  fopab2 3823  iunon 3909  iinon 3910  tfrlem8 3918  tz7.48-2 3957  tz7.49 3959  en3d 4401  onfinOLD 4520  pssnn 4534  rankr1 4674  cardnn 4824  genpss 5107  distrlem1pr 5127  renegcl 5416  redivcl 5798  uzwo4OLD 6210  nn0ind-raph 6214  uzwo 6455  uzwoOLD 6456  climconst 7094  opnneiid 7737  sncld 7787  cmsss 7997  chocuni 9172  shselt 9278  spansn 9480  spansncv 9597  findreccl 10417  hmeogrp 10538  homcard 10539  qusp 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain