Theorem sbcex 3757

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cab 2744  Vcvv 3458  [wsbc 3747

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-sbc 3748

This theorem is used by:  sbccow  3770  sbcco  3773  sbc5ALT  3776  sbcan  3796  sbcor  3797  sbcn1  3799  sbcim1  3800  sbcbi1  3804  sbcal  3806  sbcex2  3807  sbcel1v  3812  sbcel21v  3814  sbccomlem  3825  sbcrext  3829  sbcreu  3832  spesbc  3838  csbprc  4377  sbcel12  4379  sbcne12  4383  sbcel2  4386  sbccsb2  4405  sbcbr123  5170  opelopabsb  5519  csbopab  5545  csbxp  5767  csbiota  6536  csbriota  7395  fi1uzind  14564  bj-csbprc  37586  sbccomieg  43561