Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvralw.1 | |- F/ y ph |
|
cbvralw.2 | |- F/ x ps |
||
cbvralw.3 | |- ( x = y -> ( ph <-> ps ) ) |
||
Assertion | cbvralw | |- ( A. x e. A ph <-> A. y e. A ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvralw.1 | |- F/ y ph |
|
2 | cbvralw.2 | |- F/ x ps |
|
3 | cbvralw.3 | |- ( x = y -> ( ph <-> ps ) ) |
|
4 | nfcv | |- F/_ x A |
|
5 | nfcv | |- F/_ y A |
|
6 | 4 5 1 2 3 | cbvralfw | |- ( A. x e. A ph <-> A. y e. A ps ) |