Theorem sbcex 3478

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

Syntax hints:   → wi 4   ∈ wcel 2030  {cab 2637  Vcvv 3231  [wsbc 3468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469

This theorem is referenced by:  sbcco  3491  sbc5  3493  sbcan  3511  sbcor  3512  sbcn1  3514  sbcim1  3515  sbcbi1  3516  sbcal  3518  sbcex2  3519  sbcel1v  3528  sbcel21v  3530  sbcimdv  3531  sbcimdvOLD  3532  sbcrext  3544  sbcrextOLD  3545  sbcreu  3548  spesbc  3554  csbprc  4013  csbprcOLD  4014  sbcel12  4016  sbcne12  4019  sbcel2  4022  sbccsb2  4038  sbcbr123  4739  opelopabsb  5014  csbopab  5037  csbxp  5234  csbiota  5919  csbriota  6663  fi1uzind  13317  bj-csbprc  33029  sbccomieg  37674