Theorem sbcex 3729

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2716  Vcvv 3430  [wsbc 3719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-sbc 3720

This theorem is referenced by:  sbccow  3742  sbcco  3745  sbc5ALT  3748  sbcan  3771  sbcor  3772  sbcn1  3774  sbcim1  3775  sbcim1OLD  3776  sbcbi1  3781  sbcal  3784  sbcex2  3785  sbcel1v  3791  sbcel21v  3793  sbcimdvOLD  3795  sbcrext  3810  sbcreu  3813  spesbc  3819  csbprc  4345  sbcel12  4347  sbcne12  4351  sbcel2  4354  sbccsb2  4373  sbcbr123  5132  opelopabsb  5444  csbopab  5469  csbxp  5684  csbiota  6423  csbriota  7241  fi1uzind  14192  bj-csbprc  35074  sbccomieg  40595