Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv1v with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbv1.1 | |- F/ x ph |
|
cbv1.2 | |- F/ y ph |
||
cbv1.3 | |- ( ph -> F/ y ps ) |
||
cbv1.4 | |- ( ph -> F/ x ch ) |
||
cbv1.5 | |- ( ph -> ( x = y -> ( ps -> ch ) ) ) |
||
Assertion | cbv1 | |- ( ph -> ( A. x ps -> A. y ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbv1.1 | |- F/ x ph |
|
2 | cbv1.2 | |- F/ y ph |
|
3 | cbv1.3 | |- ( ph -> F/ y ps ) |
|
4 | cbv1.4 | |- ( ph -> F/ x ch ) |
|
5 | cbv1.5 | |- ( ph -> ( x = y -> ( ps -> ch ) ) ) |
|
6 | 2 3 | nfim1 | |- F/ y ( ph -> ps ) |
7 | 1 4 | nfim1 | |- F/ x ( ph -> ch ) |
8 | 5 | com12 | |- ( x = y -> ( ph -> ( ps -> ch ) ) ) |
9 | 8 | a2d | |- ( x = y -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) |
10 | 6 7 9 | cbv3 | |- ( A. x ( ph -> ps ) -> A. y ( ph -> ch ) ) |
11 | 1 | 19.21 | |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) |
12 | 2 | 19.21 | |- ( A. y ( ph -> ch ) <-> ( ph -> A. y ch ) ) |
13 | 10 11 12 | 3imtr3i | |- ( ( ph -> A. x ps ) -> ( ph -> A. y ch ) ) |
14 | 13 | pm2.86i | |- ( ph -> ( A. x ps -> A. y ch ) ) |