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

Theorem sbcel1v 3812
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2406. (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 3757 . 2 ([𝐴 / 𝑥]𝑥𝐵𝐴 ∈ V)
2 elex 3478 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3750 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2853 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb1 2892 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3527 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 381 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209  [wsb 2093  wcel 2145  Vcvv 3457  [wsbc 3747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-sbc 3748
This theorem is referenced by:  tfinds2  7848  filuni  23999  gropeld  29288  grstructeld  29289  f1od2  32972  esum2dlem  34394  bnj110  35158  f1omptsnlem  37837  relowlpssretop  37865  rdgeqoa  37871  minregex  44117  cotrclrcl  44325  frege70  44516  frege72  44518  frege91  44537  sbcoreleleq  45103  onfrALTlem4  45111  sbcoreleleqVD  45426  onfrALTlem4VD  45453  rspesbcd  45505
  Copyright terms: Public domain W3C validator