Theorem sbcex 2954

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 2947	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
2		elex 2732	. 2 |- ( A e. { x | ph } -> A e. _V )
3	1, 2	sylbi 120	1 |- ( [. A / x ]. ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 2135   {cab 2150   _Vcvv 2721   [.wsbc 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723  df-sbc 2947

This theorem is referenced by:  sbcco  2967  sbc5  2969  sbcan  2988  sbcor  2990  sbcn1  2993  sbcim1  2994  sbcbi1  2995  sbcal  2997  sbcex2  2999  sbcel1v  3008  sbcel21v  3010  sbcimdv  3011  sbcrext  3023  spesbc  3031  csbprc  3449  opelopabsb  4232