Description: Change bound variable. This is to cbvexvw what cbvaliw is to cbvalvw . TODO: move after cbvalivw . (Contributed by BJ, 17-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbvexiw.1 | |- ( E. x E. y ps -> E. y ps ) |
|
bj-cbvexiw.2 | |- ( ph -> A. y ph ) |
||
bj-cbvexiw.3 | |- ( y = x -> ( ph -> ps ) ) |
||
Assertion | bj-cbvexiw | |- ( E. x ph -> E. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbvexiw.1 | |- ( E. x E. y ps -> E. y ps ) |
|
2 | bj-cbvexiw.2 | |- ( ph -> A. y ph ) |
|
3 | bj-cbvexiw.3 | |- ( y = x -> ( ph -> ps ) ) |
|
4 | 2 3 | spimew | |- ( ph -> E. y ps ) |
5 | 1 4 | bj-sylge | |- ( E. x ph -> E. y ps ) |