ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sbcex Unicode version

Theorem sbcex 2959
Description: By our definition of proper substitution, it can only be true if the substituted expression is a set. (Contributed by Mario Carneiro, 13-Oct-2016.)
Assertion
Ref Expression
sbcex  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )

Proof of Theorem sbcex
StepHypRef Expression
1 df-sbc 2952 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 2737 . 2  |-  ( A  e.  { x  | 
ph }  ->  A  e.  _V )
31, 2sylbi 120 1  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2136   {cab 2151   _Vcvv 2726   [.wsbc 2951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147
This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728  df-sbc 2952
This theorem is referenced by:  sbcco  2972  sbc5  2974  sbcan  2993  sbcor  2995  sbcn1  2998  sbcim1  2999  sbcbi1  3000  sbcal  3002  sbcex2  3004  sbcel1v  3013  sbcel21v  3015  sbcimdv  3016  sbcrext  3028  spesbc  3036  csbprc  3454  opelopabsb  4238
  Copyright terms: Public domain W3C validator