Theorem sbcex 3782

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

Syntax hints:   → wi 4   ∈ wcel 2110  {cab 2799  Vcvv 3495  [wsbc 3772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3497  df-sbc 3773

This theorem is referenced by:  sbccow  3795  sbcco  3798  sbc5  3800  sbcan  3821  sbcor  3822  sbcn1  3824  sbcim1  3825  sbcbi1  3830  sbcal  3833  sbcex2  3834  sbcel1v  3839  sbcel1vOLD  3840  sbcel21v  3842  sbcimdv  3843  sbcrext  3856  sbcreu  3859  spesbc  3865  csbprc  4358  sbcel12  4360  sbcne12  4364  sbcel2  4367  sbccsb2  4386  sbcbr123  5113  opelopabsb  5410  csbopab  5435  csbxp  5645  csbiota  6343  csbriota  7123  fi1uzind  13849  bj-csbprc  34221  sbccomieg  39383