Theorem sbcex 3752

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2708  Vcvv 3446  [wsbc 3742

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-sbc 3743

This theorem is referenced by:  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcan  3794  sbcor  3795  sbcn1  3797  sbcim1  3798  sbcim1OLD  3799  sbcbi1  3803  sbcal  3806  sbcex2  3807  sbcel1v  3813  sbcel21v  3815  sbcimdvOLD  3817  sbcrext  3832  sbcreu  3835  spesbc  3841  csbprc  4371  sbcel12  4373  sbcne12  4377  sbcel2  4380  sbccsb2  4399  sbcbr123  5164  opelopabsb  5492  csbopab  5517  csbxp  5736  csbiota  6494  csbriota  7334  fi1uzind  14408  bj-csbprc  35453  sbccomieg  41174