Theorem sbcex 2823

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 2816	. 2 |- ( [. A / x ]. ph <-> A e. { x | ph } )
2		elex 2610	. 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 1433   {cab 2067   _Vcvv 2601   [.wsbc 2815

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-v 2603  df-sbc 2816

This theorem is referenced by:  sbcco  2836  sbc5  2838  sbcan  2856  sbcor  2858  sbcn1  2861  sbcim1  2862  sbcbi1  2863  sbcal  2865  sbcex2  2867  sbcel1v  2876  sbcel21v  2878  sbcimdv  2879  sbcrext  2891  spesbc  2899  csbprc  3289  opelopabsb  4015