HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem eleq1a 1535
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
StepHypRef Expression
1 eleq1 1526 . 2 |- (C = A -> (C e. B <-> A e. B))
21biimprcd 156 1 |- (A e. B -> (C = A -> C e. B))
Colors of variables: wff set class
Syntax hints:   -> wi 3   = wceq 953   e. wcel 955
This theorem is referenced by:  reu3 1921  uniiunlem 2122  prss 2462  tpss 2467  ordtr2 2992  peano5 3143  ssimaex 3753  fopab2 3808  iunon 3894  iinon 3895  tfrlem8 3903  tz7.48-2 3942  tz7.49 3944  en3d 4382  onfin 4499  pssnn 4513  rankr1 4646  cardnn 4796  genpss 5079  distrlem1pr 5099  renegcl 5388  redivcl 5754  uzwo4OLD 6158  nn0ind-raph 6162  uzwo 6387  uzwoOLD 6388  climconst 7031  opnneiid 7678  sncld 7726  cmsss 7931  chocuni 9088  shselt 9193  spansn 9396  spansncv 9514  findreccl 10324  hmeogrp 10425  homcard 10426  qusp 10430
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465
Copyright terms: Public domain