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

Syntax hints:   → wi 4   ∈ wcel 2141  {cab 2739  Vcvv 3453  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-sbc 3743

This theorem is referenced by:  sbccow  3765  sbcco  3768  sbc5ALT  3771  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  4360  sbcel12  4362  sbcne12  4366  sbcel2  4369  sbccsb2  4388  sbcbr123  5151  opelopabsb  5497  csbopab  5522  csbxp  5744  csbiota  6508  csbriota  7362  fi1uzind  14513  bj-csbprc  37355  sbccomieg  43330