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

Theorem sbcel1v 3477
 Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.)
Assertion
Ref Expression
sbcel1v ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
Distinct variable group:   𝑥,𝐵
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem sbcel1v
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbcex 3427 . 2 ([𝐴 / 𝑥]𝑥𝐵𝐴 ∈ V)
2 elex 3198 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3420 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2686 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb3 2726 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3253 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 368 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  [wsb 1877   ∈ wcel 1987  Vcvv 3186  [wsbc 3417 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188  df-sbc 3418 This theorem is referenced by:  tfinds2  7010  filuni  21599  gropeld  25825  grstructeld  25826  f1od2  29339  esum2dlem  29932  bnj110  30633  f1omptsnlem  32812  relowlpssretop  32841  rdgeqoa  32847  cotrclrcl  37512  frege70  37706  frege72  37708  frege91  37727  sbcoreleleq  38224  onfrALTlem4  38237
 Copyright terms: Public domain W3C validator