Theorem sbcex 3788

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2710  Vcvv 3475  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3779

This theorem is referenced by:  sbccow  3801  sbcco  3804  sbc5ALT  3807  sbcan  3830  sbcor  3831  sbcn1  3833  sbcim1  3834  sbcim1OLD  3835  sbcbi1  3839  sbcal  3842  sbcex2  3843  sbcel1v  3849  sbcel21v  3851  sbcimdvOLD  3853  sbcrext  3868  sbcreu  3871  spesbc  3877  csbprc  4407  sbcel12  4409  sbcne12  4413  sbcel2  4416  sbccsb2  4435  sbcbr123  5203  opelopabsb  5531  csbopab  5556  csbxp  5776  csbiota  6537  csbriota  7381  fi1uzind  14458  bj-csbprc  35790  sbccomieg  41531