Theorem cbvexvw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017)

	Ref	Expression
Hypothesis	cbvalvw.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvexvw	|- ( E. x ph <-> E. y ps )

Proof

Step	Hyp	Ref	Expression
1		cbvalvw.1	|- ( x = y -> ( ph <-> ps ) )
2	1	notbid	|- ( x = y -> ( -. ph <-> -. ps ) )
3	2	cbvalvw	|- ( A. x -. ph <-> A. y -. ps )
4	3	notbii	|- ( -. A. x -. ph <-> -. A. y -. ps )
5		df-ex	|- ( E. x ph <-> -. A. x -. ph )
6		df-ex	|- ( E. y ps <-> -. A. y -. ps )
7	4 5 6	3bitr4i	|- ( E. x ph <-> E. y ps )