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

Theorem sbcel2g 3272
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 3266 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  e.  C  <->  [_ A  /  x ]_ B  e.  [_ A  /  x ]_ C ) )
2 csbconstg 3265 . . 3  |-  ( A  e.  V  ->  [_ A  /  x ]_ B  =  B )
32eleq1d 2502 . 2  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ B  e.  [_ A  /  x ]_ C  <->  B  e.  [_ A  /  x ]_ C ) )
41, 3bitrd 245 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 177    e. wcel 1725   [.wsbc 3161   [_csb 3251
This theorem is referenced by:  csbcomg  3274  sbccsbg  3279  sbnfc2  3309  csbabg  3310  sbcss  3738  csbunig  4023  csbxpg  4905  csbrng  5114  issubc  14035  csbdmg  27958  sbcssOLD  28627  sbcssVD  28995  csbingVD  28996  csbunigVD  29010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-sbc 3162  df-csb 3252
  Copyright terms: Public domain W3C validator