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

Theorem sbcex 3309
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 3300 . 2  |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
2 elex 3090 . 2  |-  ( A  e.  { x  | 
ph }  ->  A  e.  _V )
31, 2sylbi 198 1  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   {cab 2407   _Vcvv 3081   [.wsbc 3299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-12 1905  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3083  df-sbc 3300
This theorem is referenced by:  sbcco  3322  sbc5  3324  sbcan  3342  sbcor  3343  sbcn1  3345  sbcim1  3346  sbcbi1  3347  sbcal  3349  sbcex2  3350  sbcel1v  3358  sbcel21v  3360  sbcimdv  3361  sbcrext  3373  sbcreu  3376  spesbc  3381  csbprc  3798  sbcel12  3800  sbcne12  3803  sbcel2  3806  sbccsb2  3822  sbcbr123  4472  opelopabsb  4726  csbopab  4748  csbxp  4931  csbiota  5590  csbriota  6275  bj-csbprc  31465  sbccomieg  35552
  Copyright terms: Public domain W3C validator