Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sbcied.1 | |- ( ph -> A e. V ) |
|
sbcied.2 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
||
Assertion | sbcied | |- ( ph -> ( [. A / x ]. ps <-> ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcied.1 | |- ( ph -> A e. V ) |
|
2 | sbcied.2 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
|
3 | nfv | |- F/ x ph |
|
4 | nfvd | |- ( ph -> F/ x ch ) |
|
5 | 1 2 3 4 | sbciedf | |- ( ph -> ( [. A / x ]. ps <-> ch ) ) |