Theorem cbveudavw

Description: Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbveudavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbveudavw	|- ( ph -> ( E! x ps <-> E! y ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbveudavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2	1	cbvexdvaw	|- ( ph -> ( E. x ps <-> E. y ch ) )
3	1	cbvmodavw	|- ( ph -> ( E* x ps <-> E* y ch ) )
4	2 3	anbi12d	|- ( ph -> ( ( E. x ps /\ E* x ps ) <-> ( E. y ch /\ E* y ch ) ) )
5		df-eu	|- ( E! x ps <-> ( E. x ps /\ E* x ps ) )
6		df-eu	|- ( E! y ch <-> ( E. y ch /\ E* y ch ) )
7	4 5 6	3bitr4g	|- ( ph -> ( E! x ps <-> E! y ch ) )