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

Theorem sbcel1v 3337
Description: Class substitution into a membership relation. (Contributed by NM, 17-Aug-2018.)
Assertion
Ref Expression
sbcel1v  |-  ( [. A  /  x ]. x  e.  B  <->  A  e.  B
)
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem sbcel1v
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 sbcex 3288 . 2  |-  ( [. A  /  x ]. x  e.  B  ->  A  e. 
_V )
2 elex 3065 . 2  |-  ( A  e.  B  ->  A  e.  _V )
3 dfsbcq2 3281 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] x  e.  B  <->  [. A  /  x ]. x  e.  B )
)
4 eleq1 2527 . . 3  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
5 clelsb3 2567 . . 3  |-  ( [ y  /  x ]
x  e.  B  <->  y  e.  B )
63, 4, 5vtoclbg 3119 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. x  e.  B  <->  A  e.  B ) )
71, 2, 6pm5.21nii 359 1  |-  ( [. A  /  x ]. x  e.  B  <->  A  e.  B
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   [wsb 1807    e. wcel 1897   _Vcvv 3056   [.wsbc 3278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279
This theorem is referenced by:  tfinds2  6716  filuni  20948  f1od2  28357  esum2dlem  28961  bnj110  29717  f1omptsnlem  31782  relowlpssretop  31811  rdgeqoa  31817  cotrclrcl  36378  frege70  36573  frege72  36575  frege91  36594  sbcoreleleq  36939  onfrALTlem4  36952  gropeld  39180  grstructeld  39181
  Copyright terms: Public domain W3C validator