Metamath Proof Explorer

Theorem sbcie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004)

Ref Expression
Hypotheses sbcie.1 A V
sbcie.2 x = A φ ψ
Assertion sbcie [˙A / x]˙ φ ψ


Step Hyp Ref Expression
1 sbcie.1 A V
2 sbcie.2 x = A φ ψ
3 2 sbcieg A V [˙A / x]˙ φ ψ
4 1 3 ax-mp [˙A / x]˙ φ ψ