MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  clelsb1 Structured version   Visualization version   GIF version

Theorem clelsb1 2867
Description: Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 2115). (Contributed by Rodolfo Medina, 28-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
clelsb1 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem clelsb1
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 eleq1w 2823 . 2 (𝑥 = 𝑤 → (𝑥𝐴𝑤𝐴))
2 eleq1w 2823 . 2 (𝑤 = 𝑦 → (𝑤𝐴𝑦𝐴))
31, 2sbievw2 2097 1 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  [wsb 2063  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clel 2815
This theorem is referenced by:  hblem  2872  hblemg  2873  eqabdv  2874  clelsb1fw  2908  clelsb1f  2909  cbvreuwOLD  3414  cbvreu  3427  elrabi  3686  sbcel1v  3855  rmo3  3888  kmlem15  10206  iuninc  32574  measiuns  34219  ballotlemodife  34501  bj-nfcf  36925  ellimcabssub0  45637
  Copyright terms: Public domain W3C validator