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

Theorem sbcel1v 3846
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2372. (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 3785 . 2 ([𝐴 / 𝑥]𝑥𝐵𝐴 ∈ V)
2 elex 3493 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3778 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2822 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb1 2861 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3558 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 380 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205  [wsb 2068  wcel 2107  Vcvv 3475  [wsbc 3775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3776
This theorem is referenced by:  tfinds2  7847  filuni  23370  gropeld  28272  grstructeld  28273  f1od2  31923  esum2dlem  33027  bnj110  33806  f1omptsnlem  36154  relowlpssretop  36182  rdgeqoa  36188  minregex  42217  cotrclrcl  42425  frege70  42616  frege72  42618  frege91  42637  sbcoreleleq  43228  onfrALTlem4  43236  sbcoreleleqVD  43552  onfrALTlem4VD  43579
  Copyright terms: Public domain W3C validator