Theorem cbvsbcdavw

Description: Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbvsbcdavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	cbvsbcdavw	|- ( ph -> ( [. A / x ]. ps <-> [. A / y ]. ch ) )

Proof

Step	Hyp	Ref	Expression
1		cbvsbcdavw.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2	1	cbvabdavw	|- ( ph -> { x | ps } = { y | ch } )
3	2	eleq2d	|- ( ph -> ( A e. { x | ps } <-> A e. { y | ch } ) )
4		df-sbc	|- ( [. A / x ]. ps <-> A e. { x | ps } )
5		df-sbc	|- ( [. A / y ]. ch <-> A e. { y | ch } )
6	3 4 5	3bitr4g	|- ( ph -> ( [. A / x ]. ps <-> [. A / y ]. ch ) )