Theorem sbcex 3738

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2714  Vcvv 3429  [wsbc 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-sbc 3729

This theorem is referenced by:  sbccow  3751  sbcco  3754  sbc5ALT  3757  sbcan  3778  sbcor  3779  sbcn1  3781  sbcim1  3782  sbcbi1  3786  sbcal  3788  sbcex2  3789  sbcel1v  3794  sbcel21v  3796  sbccomlem  3807  sbcrext  3811  sbcreu  3814  spesbc  3820  csbprc  4349  sbcel12  4351  sbcne12  4355  sbcel2  4358  sbccsb2  4377  sbcbr123  5139  opelopabsb  5485  csbopab  5510  csbxp  5732  csbiota  6491  csbriota  7339  fi1uzind  14469  bj-csbprc  37217  sbccomieg  43221