Theorem sbcex 3597

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

Syntax hints:   → wi 4   ∈ wcel 2145  {cab 2757  Vcvv 3351  [wsbc 3587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3588

This theorem is referenced by:  sbcco  3610  sbc5  3612  sbcan  3630  sbcor  3631  sbcn1  3633  sbcim1  3634  sbcbi1  3635  sbcal  3637  sbcex2  3638  sbcel1v  3646  sbcel21v  3648  sbcimdv  3649  sbcrext  3661  sbcreu  3664  spesbc  3670  csbprc  4124  csbprcOLD  4125  sbcel12  4127  sbcne12  4130  sbcel2  4133  sbccsb2  4149  sbcbr123  4840  opelopabsb  5118  csbopab  5141  csbxp  5340  csbiota  6024  csbriota  6766  fi1uzind  13481  bj-csbprc  33233  sbccomieg  37883