Theorem eleq1a 1580

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 1571	. 2 |- (C = A -> (C e. B <-> A e. B))
2	1	biimprcd 154	1 |- (A e. B -> (C = A -> C e. B))

Syntax hints:   -> wi 3   = wceq 988   e. wcel 990

This theorem is referenced by:  reu3 1969  uniiunlem 2176  prss 2519  tpss 2524  ordtr2 3057  peano5 3215  ssimaex 3844  fopab2 3899  iunon 3985  iinon 3986  tfrlem8 3994  tz7.48-2 4033  tz7.49 4035  en3d 4488  onfin 4608  pssnn 4623  iunfi 4653  rankr1 4760  cardnn 4910  genpss 5196  distrlem1pr 5216  renegcli 5505  redivcli 5882  uzwo4OLD 6323  nn0ind-raph 6327  uzwo 6515  uzwoOLD 6516  climconsti 7217  opnneiid 7857  sncld 7907  cmsss 8117  chocunii 9292  shsel 9398  spansni 9600  spansncvi 9717  findreccl 10540  hmeogrp 10674  homcard 10675  qusp 10694

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-cleq 1505  df-clel 1508

Copyright terms: Public domain