Theorem sbcex 3748

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  {cab 2738  Vcvv 3450  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sbc 3739

This theorem is used by:  sbccow  3761  sbcco  3764  sbc5ALT  3767  sbcan  3787  sbcor  3788  sbcn1  3790  sbcim1  3791  sbcbi1  3795  sbcal  3797  sbcex2  3798  sbcel1v  3803  sbcel21v  3805  sbccomlem  3816  sbcrext  3819  sbcreu  3822  spesbc  3828  csbprc  4366  sbcel12  4368  sbcne12  4372  sbcel2  4375  sbccsb2  4394  sbcbr123  5159  opelopabsb  5503  csbopab  5529  csbxp  5751  csbiota  6532  csbriota  7393  fi1uzind  14656  bj-csbprc  37915  sbccomieg  43894