Metamath Proof Explorer


Theorem bj-cbvexiw

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 )

Proof

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 )