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

Theorem sbcel1v 3842
 Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.) Avoid ax-13 2385. (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 3517 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3778 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2904 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb3 2944 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3573 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 380 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207  [wsb 2062   ∈ wcel 2107  Vcvv 3499  [wsbc 3775 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-v 3501  df-sbc 3776 This theorem is referenced by:  tfinds2  7569  filuni  22411  gropeld  26734  grstructeld  26735  f1od2  30372  esum2dlem  31239  bnj110  32018  f1omptsnlem  34488  relowlpssretop  34516  rdgeqoa  34522  cotrclrcl  39954  frege70  40146  frege72  40148  frege91  40167  sbcoreleleq  40736  onfrALTlem4  40744  sbcoreleleqVD  41060  onfrALTlem4VD  41087
 Copyright terms: Public domain W3C validator