Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 13-May-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbv1h.1 | |- ( ph -> ( ps -> A. y ps ) ) |
|
cbv1h.2 | |- ( ph -> ( ch -> A. x ch ) ) |
||
cbv1h.3 | |- ( ph -> ( x = y -> ( ps -> ch ) ) ) |
||
Assertion | cbv1h | |- ( A. x A. y ph -> ( A. x ps -> A. y ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbv1h.1 | |- ( ph -> ( ps -> A. y ps ) ) |
|
2 | cbv1h.2 | |- ( ph -> ( ch -> A. x ch ) ) |
|
3 | cbv1h.3 | |- ( ph -> ( x = y -> ( ps -> ch ) ) ) |
|
4 | nfa1 | |- F/ x A. x A. y ph |
|
5 | nfa2 | |- F/ y A. x A. y ph |
|
6 | 2sp | |- ( A. x A. y ph -> ph ) |
|
7 | 6 1 | syl | |- ( A. x A. y ph -> ( ps -> A. y ps ) ) |
8 | 5 7 | nf5d | |- ( A. x A. y ph -> F/ y ps ) |
9 | 6 2 | syl | |- ( A. x A. y ph -> ( ch -> A. x ch ) ) |
10 | 4 9 | nf5d | |- ( A. x A. y ph -> F/ x ch ) |
11 | 6 3 | syl | |- ( A. x A. y ph -> ( x = y -> ( ps -> ch ) ) ) |
12 | 4 5 8 10 11 | cbv1 | |- ( A. x A. y ph -> ( A. x ps -> A. y ch ) ) |