Metamath Proof Explorer

Theorem sbcied

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014)

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


Step Hyp Ref Expression
1 sbcied.1 φ A V
2 sbcied.2 φ x = A ψ χ
3 nfv x φ
4 nfvd φ x χ
5 1 2 3 4 sbciedf φ [˙A / x]˙ ψ χ