Theorem sbcex 3750

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 3741	. 2 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		elex 3461	. 2 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ V)
3	1, 2	sylbi 217	1 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2714  Vcvv 3440  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-sbc 3741

This theorem is referenced by:  sbccow  3763  sbcco  3766  sbc5ALT  3769  sbcan  3790  sbcor  3791  sbcn1  3793  sbcim1  3794  sbcbi1  3798  sbcal  3800  sbcex2  3801  sbcel1v  3806  sbcel21v  3808  sbccomlem  3819  sbcrext  3823  sbcreu  3826  spesbc  3832  csbprc  4361  sbcel12  4363  sbcne12  4367  sbcel2  4370  sbccsb2  4389  sbcbr123  5152  opelopabsb  5478  csbopab  5503  csbxp  5725  csbiota  6485  csbriota  7330  fi1uzind  14430  bj-csbprc  37111  sbccomieg  43035