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

Theorem sbcex 2824
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 2817 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 2611 . 2  |-  ( A  e.  { x  | 
ph }  ->  A  e.  _V )
31, 2sylbi 119 1  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   {cab 2068   _Vcvv 2602   [.wsbc 2816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604  df-sbc 2817
This theorem is referenced by:  sbcco  2837  sbc5  2839  sbcan  2857  sbcor  2859  sbcn1  2862  sbcim1  2863  sbcbi1  2864  sbcal  2866  sbcex2  2868  sbcel1v  2877  sbcel21v  2879  sbcimdv  2880  sbcrext  2892  spesbc  2900  csbprc  3290  opelopabsb  4017
  Copyright terms: Public domain W3C validator