Metamath Proof Explorer


Theorem sbciedf

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

Ref Expression
Hypotheses sbcied.1 φAV
sbcied.2 φx=Aψχ
sbciedf.3 xφ
sbciedf.4 φxχ
Assertion sbciedf φ[˙A/x]˙ψχ

Proof

Step Hyp Ref Expression
1 sbcied.1 φAV
2 sbcied.2 φx=Aψχ
3 sbciedf.3 xφ
4 sbciedf.4 φxχ
5 2 ex φx=Aψχ
6 3 5 alrimi φxx=Aψχ
7 sbciegft AVxχxx=Aψχ[˙A/x]˙ψχ
8 1 4 6 7 syl3anc φ[˙A/x]˙ψχ