Theorem sbcex 3650

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

Syntax hints:   → wi 4   ∈ wcel 2157  {cab 2799  Vcvv 3398  [wsbc 3640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-12 2215  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-v 3400  df-sbc 3641

This theorem is referenced by:  sbcco  3663  sbc5  3665  sbcan  3683  sbcor  3684  sbcn1  3686  sbcim1  3687  sbcbi1  3688  sbcal  3690  sbcex2  3691  sbcel1v  3699  sbcel21v  3701  sbcimdv  3702  sbcrext  3714  sbcreu  3717  spesbc  3723  csbprc  4185  sbcel12  4187  sbcne12  4190  sbcel2  4193  sbccsb2  4210  sbcbr123  4905  opelopabsb  5187  csbopab  5210  csbxp  5409  csbiota  6097  csbriota  6850  fi1uzind  13499  bj-csbprc  33214  sbccomieg  37860