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 φ ψ
Assertion riotarab ι x y A | ψ | χ = ι x A | φ χ

Proof

Step Hyp Ref Expression
1 riotarab.1 x = y φ ψ
2 1 bicomd x = y ψ φ
3 2 equcoms y = x ψ φ
4 3 elrab x y A | ψ x A φ
5 4 anbi1i x y A | ψ χ x A φ χ
6 anass x A φ χ x A φ χ
7 5 6 bitri x y A | ψ χ x A φ χ
8 7 iotabii ι x | x y A | ψ χ = ι x | x A φ χ
9 df-riota ι x y A | ψ | χ = ι x | x y A | ψ χ
10 df-riota ι x A | φ χ = ι x | x A φ χ
11 8 9 10 3eqtr4i ι x y A | ψ | χ = ι x A | φ χ