Theorem sbcex 3814

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2717  Vcvv 3488  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sbc 3805

This theorem is referenced by:  sbccow  3827  sbcco  3830  sbc5ALT  3833  sbcan  3857  sbcor  3858  sbcn1  3860  sbcim1  3861  sbcim1OLD  3862  sbcbi1  3866  sbcal  3868  sbcex2  3869  sbcel1v  3875  sbcel21v  3877  sbcimdvOLD  3879  sbccomlem  3891  sbcrext  3895  sbcreu  3898  spesbc  3904  csbprc  4432  sbcel12  4434  sbcne12  4438  sbcel2  4441  sbccsb2  4460  sbcbr123  5220  opelopabsb  5549  csbopab  5574  csbxp  5799  csbiota  6566  csbriota  7420  fi1uzind  14556  bj-csbprc  36876  sbccomieg  42749