Theorem sbcex 3755

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

Syntax hints:   → wi 4   ∈ wcel 2143  {cab 2741  Vcvv 3455  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-sbc 3746

This theorem is referenced by:  sbccow  3768  sbcco  3771  sbc5ALT  3774  sbcan  3794  sbcor  3795  sbcn1  3797  sbcim1  3798  sbcbi1  3802  sbcal  3804  sbcex2  3805  sbcel1v  3810  sbcel21v  3812  sbccomlem  3823  sbcrext  3827  sbcreu  3830  spesbc  3836  csbprc  4375  sbcel12  4377  sbcne12  4381  sbcel2  4384  sbccsb2  4403  sbcbr123  5166  opelopabsb  5516  csbopab  5542  csbxp  5764  csbiota  6531  csbriota  7384  fi1uzind  14546  bj-csbprc  37526  sbccomieg  43503