Theorem sbcex 2998

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 2990	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
2		elex 2774	. 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 2167   {cab 2182   _Vcvv 2763   [.wsbc 2989

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765  df-sbc 2990

This theorem is referenced by:  sbcco  3011  sbc5  3013  sbcan  3032  sbcor  3034  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbcal  3041  sbcex2  3043  sbcel1v  3052  sbcel21v  3054  sbcimdv  3055  sbcrext  3067  spesbc  3075  csbprc  3496  opelopabsb  4294