Theorem cbvmodavw

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

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

Proof

Step	Hyp	Ref	Expression
1		cbvmodavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
3	2	adantl	|- ( ( ph /\ x = y ) -> ( x = z <-> y = z ) )
4	1 3	imbi12d	|- ( ( ph /\ x = y ) -> ( ( ps -> x = z ) <-> ( ch -> y = z ) ) )
5	4	cbvaldvaw	|- ( ph -> ( A. x ( ps -> x = z ) <-> A. y ( ch -> y = z ) ) )
6	5	exbidv	|- ( ph -> ( E. z A. x ( ps -> x = z ) <-> E. z A. y ( ch -> y = z ) ) )
7		df-mo	|- ( E* x ps <-> E. z A. x ( ps -> x = z ) )
8		df-mo	|- ( E* y ch <-> E. z A. y ( ch -> y = z ) )
9	6 7 8	3bitr4g	|- ( ph -> ( E* x ps <-> E* y ch ) )