Theorem sbcex 3784

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2801  Vcvv 3496  [wsbc 3774

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498  df-sbc 3775

This theorem is referenced by:  sbccow  3797  sbcco  3800  sbc5  3802  sbcan  3823  sbcor  3824  sbcn1  3826  sbcim1  3827  sbcbi1  3832  sbcal  3835  sbcex2  3836  sbcel1v  3841  sbcel1vOLD  3842  sbcel21v  3844  sbcimdv  3845  sbcrext  3858  sbcreu  3861  spesbc  3867  csbprc  4360  sbcel12  4362  sbcne12  4366  sbcel2  4369  sbccsb2  4388  sbcbr123  5122  opelopabsb  5419  csbopab  5444  csbxp  5652  csbiota  6350  csbriota  7131  fi1uzind  13858  bj-csbprc  34228  sbccomieg  39397