Theorem cbvsbcvw2

Description: Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	cbvsbcvw2.1	|- A = B
	cbvsbcvw2.2	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvsbcvw2	|- ( [. A / x ]. ph <-> [. B / y ]. ps )

Proof

Step	Hyp	Ref	Expression
1		cbvsbcvw2.1	|- A = B
2		cbvsbcvw2.2	|- ( x = y -> ( ph <-> ps ) )
3	2	cbvabv	|- { x | ph } = { y | ps }
4	1 3	eleq12i	|- ( A e. { x | ph } <-> B e. { y | ps } )
5		df-sbc	|- ( [. A / x ]. ph <-> A e. { x | ph } )
6		df-sbc	|- ( [. B / y ]. ps <-> B e. { y | ps } )
7	4 5 6	3bitr4i	|- ( [. A / x ]. ph <-> [. B / y ]. ps )