Theorem sbcex 3757

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	⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

Proof of Theorem sbcex

Step	Hyp	Ref	Expression
1		df-sbc 3748	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		elex 3478	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V)
3	1, 2	sylbi 220	1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2145  {cab 2743  Vcvv 3457  [wsbc 3747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-sbc 3748

This theorem is referenced by:  sbccow  3770  sbcco  3773  sbc5ALT  3776  sbcan  3796  sbcor  3797  sbcn1  3799  sbcim1  3800  sbcbi1  3804  sbcal  3806  sbcex2  3807  sbcel1v  3812  sbcel21v  3814  sbccomlem  3825  sbcrext  3829  sbcreu  3832  spesbc  3838  csbprc  4366  sbcel12  4368  sbcne12  4372  sbcel2  4375  sbccsb2  4394  sbcbr123  5158  opelopabsb  5504  csbopab  5530  csbxp  5752  csbiota  6518  csbriota  7372  fi1uzind  14532  bj-csbprc  37402  sbccomieg  43377