Theorem sbcex 3736

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

Syntax hints:   → wi 4   ∈ wcel 2105  {cab 2714  Vcvv 3441  [wsbc 3726

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-sbc 3727

This theorem is referenced by:  sbccow  3749  sbcco  3752  sbc5ALT  3755  sbcan  3778  sbcor  3779  sbcn1  3781  sbcim1  3782  sbcim1OLD  3783  sbcbi1  3787  sbcal  3790  sbcex2  3791  sbcel1v  3797  sbcel21v  3799  sbcimdvOLD  3801  sbcrext  3816  sbcreu  3819  spesbc  3825  csbprc  4351  sbcel12  4353  sbcne12  4357  sbcel2  4360  sbccsb2  4379  sbcbr123  5141  opelopabsb  5463  csbopab  5488  csbxp  5705  csbiota  6459  csbriota  7290  fi1uzind  14290  bj-csbprc  35168  sbccomieg  40831