Theorem riotaeqbii

Description: Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	riotaeqbii.1	|- A = B
	riotaeqbii.2	|- ( ph <-> ps )
Assertion	riotaeqbii	|- ( iota_ x e. A ph ) = ( iota_ x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		riotaeqbii.1	|- A = B
2		riotaeqbii.2	|- ( ph <-> ps )
3	1	eleq2i	|- ( x e. A <-> x e. B )
4	3 2	anbi12i	|- ( ( x e. A /\ ph ) <-> ( x e. B /\ ps ) )
5	4	iotabii	|- ( iota x ( x e. A /\ ph ) ) = ( iota x ( x e. B /\ ps ) )
6		df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
7		df-riota	|- ( iota_ x e. B ps ) = ( iota x ( x e. B /\ ps ) )
8	5 6 7	3eqtr4i	|- ( iota_ x e. A ph ) = ( iota_ x e. B ps )