Theorem sbcex 3752

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2715  Vcvv 3442  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-sbc 3743

This theorem is referenced by:  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3792  sbcor  3793  sbcn1  3795  sbcim1  3796  sbcbi1  3800  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcel21v  3810  sbccomlem  3821  sbcrext  3825  sbcreu  3828  spesbc  3834  csbprc  4363  sbcel12  4365  sbcne12  4369  sbcel2  4372  sbccsb2  4391  sbcbr123  5154  opelopabsb  5486  csbopab  5511  csbxp  5733  csbiota  6493  csbriota  7340  fi1uzind  14442  bj-csbprc  37155  sbccomieg  43147