Theorem sbcex 3746

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

Syntax hints:   → wi 4   ∈ wcel 2111  {cab 2709  Vcvv 3436  [wsbc 3736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sbc 3737

This theorem is referenced by:  sbccow  3759  sbcco  3762  sbc5ALT  3765  sbcan  3786  sbcor  3787  sbcn1  3789  sbcim1  3790  sbcbi1  3794  sbcal  3796  sbcex2  3797  sbcel1v  3802  sbcel21v  3804  sbccomlem  3815  sbcrext  3819  sbcreu  3822  spesbc  3828  csbprc  4358  sbcel12  4360  sbcne12  4364  sbcel2  4367  sbccsb2  4386  sbcbr123  5147  opelopabsb  5473  csbopab  5498  csbxp  5720  csbiota  6480  csbriota  7324  fi1uzind  14420  bj-csbprc  36961  sbccomieg  42891