Theorem cbveuvw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbveu for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 25-Nov-1994) (Revised by GG, 30-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbveuvw.1	|- ( x = y -> ( ph <-> ps ) )
2	1	cbvexvw	|- ( E. x ph <-> E. y ps )
3	1	cbvmovw	|- ( E* x ph <-> E* y ps )
4	2 3	anbi12i	|- ( ( E. x ph /\ E* x ph ) <-> ( E. y ps /\ E* y ps ) )
5		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
6		df-eu	|- ( E! y ps <-> ( E. y ps /\ E* y ps ) )
7	4 5 6	3bitr4i	|- ( E! x ph <-> E! y ps )