Theorem sbcex 3754

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707  Vcvv 3438  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-sbc 3745

This theorem is referenced by:  sbccow  3767  sbcco  3770  sbc5ALT  3773  sbcan  3794  sbcor  3795  sbcn1  3797  sbcim1  3798  sbcbi1  3802  sbcal  3804  sbcex2  3805  sbcel1v  3810  sbcel21v  3812  sbccomlem  3823  sbcrext  3827  sbcreu  3830  spesbc  3836  csbprc  4362  sbcel12  4364  sbcne12  4368  sbcel2  4371  sbccsb2  4390  sbcbr123  5149  opelopabsb  5477  csbopab  5502  csbxp  5723  csbiota  6479  csbriota  7325  fi1uzind  14432  bj-csbprc  36886  sbccomieg  42769