Theorem sbcex 3014

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 3006	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
2		elex 2788	. 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 2178   {cab 2193   _Vcvv 2776   [.wsbc 3005

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778  df-sbc 3006

This theorem is referenced by:  sbcco  3027  sbc5  3029  sbcan  3048  sbcor  3050  sbcn1  3053  sbcim1  3054  sbcbi1  3055  sbcal  3057  sbcex2  3059  sbcel1v  3068  sbcel21v  3070  sbcimdv  3071  sbcrext  3083  spesbc  3092  csbprc  3514  opelopabsb  4324