Theorem eleq1a 1540

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 1531	. 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 954   e. wcel 956

This theorem is referenced by:  reu3 1927  uniiunlem 2128  prss 2467  tpss 2472  ordtr2 2997  peano5 3148  ssimaex 3759  fopab2 3814  iunon 3900  iinon 3901  tfrlem8 3909  tz7.48-2 3948  tz7.49 3950  en3d 4388  onfin 4505  pssnn 4519  rankr1 4654  cardnn 4804  genpss 5087  distrlem1pr 5107  renegcl 5396  redivcl 5762  uzwo4OLD 6166  nn0ind-raph 6170  uzwo 6395  uzwoOLD 6396  climconst 7039  opnneiid 7687  sncld 7737  cmsss 7947  chocuni 9111  shselt 9216  spansn 9419  spansncv 9537  findreccl 10351  hmeogrp 10461  homcard 10462  qusp 10466

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain