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