Theorem sbcex 3731

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

Syntax hints:   → wi 4   ∈ wcel 2104  {cab 2713  Vcvv 3437  [wsbc 3721

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-sbc 3722

This theorem is referenced by:  sbccow  3744  sbcco  3747  sbc5ALT  3750  sbcan  3773  sbcor  3774  sbcn1  3776  sbcim1  3777  sbcim1OLD  3778  sbcbi1  3782  sbcal  3785  sbcex2  3786  sbcel1v  3792  sbcel21v  3794  sbcimdvOLD  3796  sbcrext  3811  sbcreu  3814  spesbc  3820  csbprc  4346  sbcel12  4348  sbcne12  4352  sbcel2  4355  sbccsb2  4374  sbcbr123  5135  opelopabsb  5456  csbopab  5481  csbxp  5697  csbiota  6451  csbriota  7280  fi1uzind  14260  bj-csbprc  35143  sbccomieg  40810