Theorem sbcex 2971

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

Syntax hints:   → wi 4   ∈ wcel 2148  {cab 2163  Vcvv 2737  [wsbc 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739  df-sbc 2963

This theorem is referenced by:  sbcco  2984  sbc5  2986  sbcan  3005  sbcor  3007  sbcn1  3010  sbcim1  3011  sbcbi1  3012  sbcal  3014  sbcex2  3016  sbcel1v  3025  sbcel21v  3027  sbcimdv  3028  sbcrext  3040  spesbc  3048  csbprc  3468  opelopabsb  4260