Theorem sbcex 3763

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707  Vcvv 3447  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-sbc 3754

This theorem is referenced by:  sbccow  3776  sbcco  3779  sbc5ALT  3782  sbcan  3803  sbcor  3804  sbcn1  3806  sbcim1  3807  sbcbi1  3811  sbcal  3813  sbcex2  3814  sbcel1v  3819  sbcel21v  3821  sbccomlem  3832  sbcrext  3836  sbcreu  3839  spesbc  3845  csbprc  4372  sbcel12  4374  sbcne12  4378  sbcel2  4381  sbccsb2  4400  sbcbr123  5161  opelopabsb  5490  csbopab  5515  csbxp  5738  csbiota  6504  csbriota  7359  fi1uzind  14472  bj-csbprc  36898  sbccomieg  42781