Theorem sbcex 3766

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2708  Vcvv 3450  [wsbc 3756

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sbc 3757

This theorem is referenced by:  sbccow  3779  sbcco  3782  sbc5ALT  3785  sbcan  3806  sbcor  3807  sbcn1  3809  sbcim1  3810  sbcbi1  3814  sbcal  3816  sbcex2  3817  sbcel1v  3822  sbcel21v  3824  sbccomlem  3835  sbcrext  3839  sbcreu  3842  spesbc  3848  csbprc  4375  sbcel12  4377  sbcne12  4381  sbcel2  4384  sbccsb2  4403  sbcbr123  5164  opelopabsb  5493  csbopab  5518  csbxp  5741  csbiota  6507  csbriota  7362  fi1uzind  14479  bj-csbprc  36905  sbccomieg  42788