Theorem bj-cbvexw

Description: Change bound variable. This is to cbvexvw what cbvalw is to cbvalvw . (Contributed by BJ, 17-Mar-2020)

	Ref	Expression
Hypotheses	bj-cbvexw.1	|- ( E. x E. y ps -> E. y ps )
	bj-cbvexw.2	|- ( ph -> A. y ph )
	bj-cbvexw.3	|- ( E. y E. x ph -> E. x ph )
	bj-cbvexw.4	|- ( ps -> A. x ps )
	bj-cbvexw.5	|- ( x = y -> ( ph <-> ps ) )
Assertion	bj-cbvexw	|- ( E. x ph <-> E. y ps )

Proof

Step	Hyp	Ref	Expression
1		bj-cbvexw.1	|- ( E. x E. y ps -> E. y ps )
2		bj-cbvexw.2	|- ( ph -> A. y ph )
3		bj-cbvexw.3	|- ( E. y E. x ph -> E. x ph )
4		bj-cbvexw.4	|- ( ps -> A. x ps )
5		bj-cbvexw.5	|- ( x = y -> ( ph <-> ps ) )
6	5	equcoms	|- ( y = x -> ( ph <-> ps ) )
7	6	biimpd	|- ( y = x -> ( ph -> ps ) )
8	1 2 7	bj-cbvexiw	|- ( E. x ph -> E. y ps )
9	5	biimprd	|- ( x = y -> ( ps -> ph ) )
10	3 4 9	bj-cbvexiw	|- ( E. y ps -> E. x ph )
11	8 10	impbii	|- ( E. x ph <-> E. y ps )