Theorem sbcex 3412

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

Syntax hints:   → wi 4   ∈ wcel 1977  {cab 2596  Vcvv 3173  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403

This theorem is referenced by:  sbcco  3425  sbc5  3427  sbcan  3445  sbcor  3446  sbcn1  3448  sbcim1  3449  sbcbi1  3450  sbcal  3452  sbcex2  3453  sbcel1v  3462  sbcel21v  3464  sbcimdv  3465  sbcimdvOLD  3466  sbcrext  3478  sbcrextOLD  3479  sbcreu  3482  spesbc  3487  csbprc  3932  csbprcOLD  3933  sbcel12  3935  sbcne12  3938  sbcel2  3941  sbccsb2  3957  sbcbr123  4636  opelopabsb  4910  csbopab  4932  csbxp  5123  csbiota  5797  csbriota  6523  fi1uzind  13134  fi1uzindOLD  13140  bj-csbprc  32096  sbccomieg  36375