Theorem cbvals

Description: Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Hypotheses	cbvals.1	|- ( x = y -> ( ph <-> ch ) )
	cbvals.2	|- ( x = y -> ( ps <-> th ) )
Assertion	cbvals	|- ( AE x ( ph -> ps ) <-> AE y ( ch -> th ) )

Proof

Step	Hyp	Ref	Expression
1		cbvals.1	|- ( x = y -> ( ph <-> ch ) )
2		cbvals.2	|- ( x = y -> ( ps <-> th ) )
3	1 2	imbi12d	|- ( x = y -> ( ( ph -> ps ) <-> ( ch -> th ) ) )
4	3	cbvalvw	|- ( A. x ( ph -> ps ) <-> A. y ( ch -> th ) )
5	1	cbvexvw	|- ( E. x ph <-> E. y ch )
6	4 5	anbi12i	|- ( ( A. x ( ph -> ps ) /\ E. x ph ) <-> ( A. y ( ch -> th ) /\ E. y ch ) )
7		df-als	|- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
8		df-als	|- ( AE y ( ch -> th ) <-> ( A. y ( ch -> th ) /\ E. y ch ) )
9	6 7 8	3bitr4i	|- ( AE x ( ph -> ps ) <-> AE y ( ch -> th ) )