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

Theorem sbcex 3321
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 3312 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 3102 . 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 1802   {cab 2426   _Vcvv 3093   [.wsbc 3311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095  df-sbc 3312
This theorem is referenced by:  sbcco  3334  sbc5  3336  sbcan  3354  sbcor  3356  sbcn1  3359  sbcim1  3360  sbcbi1  3361  sbcal  3363  sbcex2  3365  sbcel1v  3376  sbcel21v  3379  sbcimdv  3380  sbcrext  3394  sbcreu  3398  spesbc  3404  csbprc  3803  sbcel12  3805  sbcne12  3809  sbcel2  3813  sbccsb2  3833  sbcbr123  4484  opelopabsb  4743  csbopab  4765  csbxp  5067  csbiota  5566  csbriota  6250  sbccomieg  30694  bj-csbprc  34188
  Copyright terms: Public domain W3C validator