This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )