Theorem sbcex 3800

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

Syntax hints:   → wi 4   ∈ wcel 2105  {cab 2711  Vcvv 3477  [wsbc 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sbc 3791

This theorem is referenced by:  sbccow  3813  sbcco  3816  sbc5ALT  3819  sbcan  3843  sbcor  3844  sbcn1  3846  sbcim1  3847  sbcim1OLD  3848  sbcbi1  3852  sbcal  3854  sbcex2  3855  sbcel1v  3861  sbcel21v  3863  sbcimdvOLD  3865  sbccomlem  3877  sbcrext  3881  sbcreu  3884  spesbc  3890  csbprc  4414  sbcel12  4416  sbcne12  4420  sbcel2  4423  sbccsb2  4442  sbcbr123  5201  opelopabsb  5539  csbopab  5564  csbxp  5787  csbiota  6555  csbriota  7402  fi1uzind  14542  bj-csbprc  36892  sbccomieg  42780