Theorem cbvmovw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvmo for a version 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		df-mo	|- ( E* x ph <-> E. z A. x ( ph -> x = z ) )
3		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
4	1 3	imbi12d	|- ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) )
5	4	cbvalvw	|- ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) )
6	5	exbii	|- ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) )
7		df-mo	|- ( E* y ps <-> E. z A. y ( ps -> y = z ) )
8	7	bicomi	|- ( E. z A. y ( ps -> y = z ) <-> E* y ps )
9	2 6 8	3bitri	|- ( E* x ph <-> E* y ps )