Theorem sbcex 2824

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

Syntax hints:   -> wi 4   e. wcel 1434   {cab 2068   _Vcvv 2602   [.wsbc 2816

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604  df-sbc 2817

This theorem is referenced by:  sbcco  2837  sbc5  2839  sbcan  2857  sbcor  2859  sbcn1  2862  sbcim1  2863  sbcbi1  2864  sbcal  2866  sbcex2  2868  sbcel1v  2877  sbcel21v  2879  sbcimdv  2880  sbcrext  2892  spesbc  2900  csbprc  3290  opelopabsb  4017