Theorem sbcex 3693

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

Syntax hints:   → wi 4   ∈ wcel 2112  {cab 2714  Vcvv 3398  [wsbc 3683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-sbc 3684

This theorem is referenced by:  sbccow  3706  sbcco  3709  sbc5ALT  3712  sbcan  3735  sbcor  3736  sbcn1  3738  sbcim1  3739  sbcbi1  3744  sbcal  3747  sbcex2  3748  sbcel1v  3753  sbcel21v  3755  sbcimdvOLD  3757  sbcrext  3772  sbcreu  3775  spesbc  3781  csbprc  4307  sbcel12  4309  sbcne12  4313  sbcel2  4316  sbccsb2  4335  sbcbr123  5093  opelopabsb  5396  csbopab  5421  csbxp  5632  csbiota  6351  csbriota  7164  fi1uzind  14028  bj-csbprc  34782  sbccomieg  40259