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

Theorem sbcel2g 3115
Description: Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005.)
Assertion
Ref Expression
sbcel2g  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  e.  C  <->  B  e.  [_ A  /  x ]_ C ) )
Distinct variable group:    x, B
Allowed substitution hints:    A( x)    C( x)    V( x)

Proof of Theorem sbcel2g
StepHypRef Expression
1 sbcel12g 3109 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  e.  C  <->  [_ A  /  x ]_ B  e.  [_ A  /  x ]_ C ) )
2 csbconstg 3108 . . 3  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  B )
32eleq1d 2362 . 2  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ B  e.  [_ A  /  x ]_ C  <->  B  e.  [_ A  /  x ]_ C ) )
41, 3bitrd 244 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  e.  C  <->  B  e.  [_ A  /  x ]_ C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1696   [.wsbc 3004   [_csb 3094
This theorem is referenced by:  csbcomg  3117  sbccsbg  3122  sbnfc2  3154  csbabg  3155  sbcss  3577  csbunig  3851  csbxpg  4732  csbrng  4939  issubc  13728  csbdmg  28085  sbcssOLD  28605  sbcssVD  28975  csbingVD  28976  csbunigVD  28990
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator