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

Theorem sbcel1v 3848
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2371. (Revised by Wolf Lammen, 30-Apr-2023.)
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 3787 . 2 ([𝐴 / 𝑥]𝑥𝐵𝐴 ∈ V)
2 elex 3492 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3780 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2821 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb1 2860 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3559 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 379 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  [wsb 2067  wcel 2106  Vcvv 3474  [wsbc 3777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-sbc 3778
This theorem is referenced by:  tfinds2  7855  filuni  23609  gropeld  28548  grstructeld  28549  f1od2  32201  esum2dlem  33376  bnj110  34155  f1omptsnlem  36520  relowlpssretop  36548  rdgeqoa  36554  minregex  42587  cotrclrcl  42795  frege70  42986  frege72  42988  frege91  43007  sbcoreleleq  43598  onfrALTlem4  43606  sbcoreleleqVD  43922  onfrALTlem4VD  43949
  Copyright terms: Public domain W3C validator