Theorem sbcex 3798

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2714  Vcvv 3480  [wsbc 3788

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sbc 3789

This theorem is referenced by:  sbccow  3811  sbcco  3814  sbc5ALT  3817  sbcan  3838  sbcor  3839  sbcn1  3841  sbcim1  3842  sbcim1OLD  3843  sbcbi1  3847  sbcal  3849  sbcex2  3850  sbcel1v  3856  sbcel21v  3858  sbccomlem  3869  sbcrext  3873  sbcreu  3876  spesbc  3882  csbprc  4409  sbcel12  4411  sbcne12  4415  sbcel2  4418  sbccsb2  4437  sbcbr123  5197  opelopabsb  5535  csbopab  5560  csbxp  5785  csbiota  6554  csbriota  7403  fi1uzind  14546  bj-csbprc  36911  sbccomieg  42804