Theorem cbvrabdavw2

Description: Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypotheses	cbvrabdavw2.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
	cbvrabdavw2.2	|- ( ( ph /\ x = y ) -> A = B )
Assertion	cbvrabdavw2	|- ( ph -> { x e. A | ps } = { y e. B | ch } )

Proof

Step	Hyp	Ref	Expression
1		cbvrabdavw2.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2		cbvrabdavw2.2	|- ( ( ph /\ x = y ) -> A = B )
3		eleq1w	|- ( x = y -> ( x e. A <-> y e. A ) )
4	3	adantl	|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. A ) )
5	2	eleq2d	|- ( ( ph /\ x = y ) -> ( y e. A <-> y e. B ) )
6	4 5	bitrd	|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. B ) )
7	6 1	anbi12d	|- ( ( ph /\ x = y ) -> ( ( x e. A /\ ps ) <-> ( y e. B /\ ch ) ) )
8	7	cbvabdavw	|- ( ph -> { x | ( x e. A /\ ps ) } = { y | ( y e. B /\ ch ) } )
9		df-rab	|- { x e. A | ps } = { x | ( x e. A /\ ps ) }
10		df-rab	|- { y e. B | ch } = { y | ( y e. B /\ ch ) }
11	8 9 10	3eqtr4g	|- ( ph -> { x e. A | ps } = { y e. B | ch } )