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

Theorem sbcex 3208
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 3199 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 2993 . 2  |-  ( A  e.  { x  | 
ph }  ->  A  e.  _V )
31, 2sylbi 195 1  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   {cab 2429   _Vcvv 2984   [.wsbc 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2986  df-sbc 3199
This theorem is referenced by:  sbcco  3221  sbc5  3223  sbcan  3241  sbcor  3243  sbcn1  3246  sbcim1  3247  sbcbi1  3248  sbcal  3250  sbcex2  3252  sbcel1v  3263  sbcel21v  3266  sbcimdv  3267  sbcrext  3281  sbcreu  3285  spesbc  3291  csbprc  3685  sbcel12  3687  sbcne12  3691  sbcel2  3695  sbccsb2  3715  sbcbr123  4355  opelopabsb  4611  csbopab  4632  csbxp  4930  csbiota  5422  csbriota  6076  sbccomieg  29143  bj-csbprc  32423
  Copyright terms: Public domain W3C validator