Theorem riotarab

Description: Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Hypothesis	riotarab.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	riotarab	|- ( iota_ x e. { y e. A | ps } ch ) = ( iota_ x e. A ( ph /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		riotarab.1	|- ( x = y -> ( ph <-> ps ) )
2	1	bicomd	|- ( x = y -> ( ps <-> ph ) )
3	2	equcoms	|- ( y = x -> ( ps <-> ph ) )
4	3	elrab	|- ( x e. { y e. A | ps } <-> ( x e. A /\ ph ) )
5	4	anbi1i	|- ( ( x e. { y e. A | ps } /\ ch ) <-> ( ( x e. A /\ ph ) /\ ch ) )
6		anass	|- ( ( ( x e. A /\ ph ) /\ ch ) <-> ( x e. A /\ ( ph /\ ch ) ) )
7	5 6	bitri	|- ( ( x e. { y e. A | ps } /\ ch ) <-> ( x e. A /\ ( ph /\ ch ) ) )
8	7	iotabii	|- ( iota x ( x e. { y e. A | ps } /\ ch ) ) = ( iota x ( x e. A /\ ( ph /\ ch ) ) )
9		df-riota	|- ( iota_ x e. { y e. A | ps } ch ) = ( iota x ( x e. { y e. A | ps } /\ ch ) )
10		df-riota	|- ( iota_ x e. A ( ph /\ ch ) ) = ( iota x ( x e. A /\ ( ph /\ ch ) ) )
11	8 9 10	3eqtr4i	|- ( iota_ x e. { y e. A | ps } ch ) = ( iota_ x e. A ( ph /\ ch ) )