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  24003  gropeld  29292  grstructeld  29293  f1od2  32976  esum2dlem  34399  bnj110  35163  f1omptsnlem  37842  relowlpssretop  37870  rdgeqoa  37876  minregex  44122  cotrclrcl  44330  frege70  44521  frege72  44523  frege91  44542  sbcoreleleq  45109  onfrALTlem4  45117  sbcoreleleqVD  45432  onfrALTlem4VD  45459  rspesbcd  45511
  Copyright terms: Public domain W3C validator