Metamath Proof Explorer

Theorem sbcex

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)

Ref Expression
Assertion sbcex [˙A / x]˙ φ A V


Step Hyp Ref Expression
1 df-sbc [˙A / x]˙ φ A x | φ
2 elex A x | φ A V
3 1 2 sylbi [˙A / x]˙ φ A V