Theorem sbcex 3445

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

Syntax hints:   -> wi 4   e. wcel 1990   {cab 2608   _Vcvv 3200   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-sbc 3436

This theorem is referenced by:  sbcco  3458  sbc5  3460  sbcan  3478  sbcor  3479  sbcn1  3481  sbcim1  3482  sbcbi1  3483  sbcal  3485  sbcex2  3486  sbcel1v  3495  sbcel21v  3497  sbcimdv  3498  sbcimdvOLD  3499  sbcrext  3511  sbcrextOLD  3512  sbcreu  3515  spesbc  3521  csbprc  3980  csbprcOLD  3981  sbcel12  3983  sbcne12  3986  sbcel2  3989  sbccsb2  4005  sbcbr123  4706  opelopabsb  4985  csbopab  5008  csbxp  5200  csbiota  5881  csbriota  6623  fi1uzind  13279  fi1uzindOLD  13285  bj-csbprc  32904  sbccomieg  37357