Theorem sbcex 3749

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cab 2739  Vcvv 3451  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-sbc 3740

This theorem is used by:  sbccow  3762  sbcco  3765  sbc5ALT  3768  sbcan  3788  sbcor  3789  sbcn1  3791  sbcim1  3792  sbcbi1  3796  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcel21v  3806  sbccomlem  3817  sbcrext  3820  sbcreu  3823  spesbc  3829  csbprc  4367  sbcel12  4369  sbcne12  4373  sbcel2  4376  sbccsb2  4395  sbcbr123  5159  opelopabsb  5504  csbopab  5530  csbxp  5752  csbiota  6524  csbriota  7384  fi1uzind  14632  bj-csbprc  37792  sbccomieg  43753