Theorem cbvmovw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvmo and cbvmow for versions with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Mar-1995) (Revised by Gino Giotto, 30-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmovw.1	|- ( x = y -> ( ph <-> ps ) )
2		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
3	1 2	imbi12d	|- ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) )
4	3	cbvalvw	|- ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) )
5	4	exbii	|- ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) )
6		df-mo	|- ( E* x ph <-> E. z A. x ( ph -> x = z ) )
7		df-mo	|- ( E* y ps <-> E. z A. y ( ps -> y = z ) )
8	5 6 7	3bitr4i	|- ( E* x ph <-> E* y ps )