Theorem sbcex 3007

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

Step	Hyp	Ref	Expression
1		df-sbc 2999	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
2		elex 2783	. 2 |- ( A e. { x | ph } -> A e. _V )
3	1, 2	sylbi 121	1 |- ( [. A / x ]. ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 2176   {cab 2191   _Vcvv 2772   [.wsbc 2998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774  df-sbc 2999

This theorem is referenced by:  sbcco  3020  sbc5  3022  sbcan  3041  sbcor  3043  sbcn1  3046  sbcim1  3047  sbcbi1  3048  sbcal  3050  sbcex2  3052  sbcel1v  3061  sbcel21v  3063  sbcimdv  3064  sbcrext  3076  spesbc  3084  csbprc  3506  opelopabsb  4306