Theorem cbvsbcvw

Description: Change the bound variable of a class substitution using implicit substitution. Version of cbvsbcv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 30-Sep-2008) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

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