Theorem sbcex 3751

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

Syntax hints:   → wi 4   ∈ wcel 2111  {cab 2709  Vcvv 3436  [wsbc 3741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sbc 3742

This theorem is referenced by:  sbccow  3764  sbcco  3767  sbc5ALT  3770  sbcan  3791  sbcor  3792  sbcn1  3794  sbcim1  3795  sbcbi1  3799  sbcal  3801  sbcex2  3802  sbcel1v  3807  sbcel21v  3809  sbccomlem  3820  sbcrext  3824  sbcreu  3827  spesbc  3833  csbprc  4359  sbcel12  4361  sbcne12  4365  sbcel2  4368  sbccsb2  4387  sbcbr123  5145  opelopabsb  5470  csbopab  5495  csbxp  5716  csbiota  6474  csbriota  7318  fi1uzind  14414  bj-csbprc  36950  sbccomieg  42832