Theorem sbcex 3747

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2711  Vcvv 3437  [wsbc 3737

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-sbc 3738

This theorem is referenced by:  sbccow  3760  sbcco  3763  sbc5ALT  3766  sbcan  3787  sbcor  3788  sbcn1  3790  sbcim1  3791  sbcbi1  3795  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbcel21v  3805  sbccomlem  3816  sbcrext  3820  sbcreu  3823  spesbc  3829  csbprc  4358  sbcel12  4360  sbcne12  4364  sbcel2  4367  sbccsb2  4386  sbcbr123  5149  opelopabsb  5475  csbopab  5500  csbxp  5722  csbiota  6481  csbriota  7326  fi1uzind  14418  bj-csbprc  36977  sbccomieg  42913