Theorem sbcex 3775

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2713  Vcvv 3459  [wsbc 3765

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sbc 3766

This theorem is referenced by:  sbccow  3788  sbcco  3791  sbc5ALT  3794  sbcan  3815  sbcor  3816  sbcn1  3818  sbcim1  3819  sbcbi1  3823  sbcal  3825  sbcex2  3826  sbcel1v  3831  sbcel21v  3833  sbccomlem  3844  sbcrext  3848  sbcreu  3851  spesbc  3857  csbprc  4384  sbcel12  4386  sbcne12  4390  sbcel2  4393  sbccsb2  4412  sbcbr123  5173  opelopabsb  5505  csbopab  5530  csbxp  5754  csbiota  6524  csbriota  7377  fi1uzind  14525  bj-csbprc  36928  sbccomieg  42816