Theorem sbcex 3740

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

Syntax hints:   → wi 4   ∈ wcel 2119  {cab 2718  Vcvv 3432  [wsbc 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-sbc 3731

This theorem is referenced by:  sbccow  3753  sbcco  3756  sbc5ALT  3759  sbcan  3779  sbcor  3780  sbcn1  3782  sbcim1  3783  sbcbi1  3787  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbcel21v  3797  sbccomlem  3808  sbcrext  3812  sbcreu  3815  spesbc  3821  csbprc  4344  sbcel12  4346  sbcne12  4350  sbcel2  4353  sbccsb2  4372  sbcbr123  5133  opelopabsb  5479  csbopab  5504  csbxp  5726  csbiota  6485  csbriota  7335  fi1uzind  14467  bj-csbprc  37270  sbccomieg  43245