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

Theorem sbcel1v 3703
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.)
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 3654 . 2 ([𝐴 / 𝑥]𝑥𝐵𝐴 ∈ V)
2 elex 3417 . 2 (𝐴𝐵𝐴 ∈ V)
3 dfsbcq2 3647 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝑥𝐵[𝐴 / 𝑥]𝑥𝐵))
4 eleq1 2884 . . 3 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
5 clelsb3 2924 . . 3 ([𝑦 / 𝑥]𝑥𝐵𝑦𝐵)
63, 4, 5vtoclbg 3471 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵))
71, 2, 6pm5.21nii 369 1 ([𝐴 / 𝑥]𝑥𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  [wsb 2061  wcel 2157  Vcvv 3402  [wsbc 3644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-v 3404  df-sbc 3645
This theorem is referenced by:  tfinds2  7300  filuni  21910  gropeld  26149  grstructeld  26150  f1od2  29836  esum2dlem  30489  bnj110  31260  f1omptsnlem  33506  relowlpssretop  33534  rdgeqoa  33540  cotrclrcl  38539  frege70  38732  frege72  38734  frege91  38753  sbcoreleleq  39248  onfrALTlem4  39261
  Copyright terms: Public domain W3C validator