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

Theorem sbcex 3265
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 3256 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 3040 . 2  |-  ( A  e.  { x  | 
ph }  ->  A  e.  _V )
31, 2sylbi 200 1  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   {cab 2457   _Vcvv 3031   [.wsbc 3255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033  df-sbc 3256
This theorem is referenced by:  sbcco  3278  sbc5  3280  sbcan  3298  sbcor  3299  sbcn1  3301  sbcim1  3302  sbcbi1  3303  sbcal  3305  sbcex2  3306  sbcel1v  3314  sbcel21v  3316  sbcimdv  3317  sbcrext  3329  sbcreu  3332  spesbc  3337  csbprc  3774  sbcel12  3776  sbcne12  3779  sbcel2  3782  sbccsb2  3798  sbcbr123  4447  opelopabsb  4711  csbopab  4733  csbxp  4921  csbiota  5582  csbriota  6282  fi1uzind  12691  fi1uzindOLD  12697  bj-csbprc  31579  sbccomieg  35707
  Copyright terms: Public domain W3C validator