Theorem cbvriotadavw2

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

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

Proof

Step	Hyp	Ref	Expression
1		cbvriotadavw2.1	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
2		cbvriotadavw2.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	cbviotadavw	|- ( ph -> ( iota x ( x e. A /\ ps ) ) = ( iota y ( y e. B /\ ch ) ) )
9		df-riota	|- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
10		df-riota	|- ( iota_ y e. B ch ) = ( iota y ( y e. B /\ ch ) )
11	8 9 10	3eqtr4g	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ y e. B ch ) )