Metamath Proof Explorer


Theorem riotabidv

Description: Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011)

Ref Expression
Hypothesis riotabidv.1 φ ψ χ
Assertion riotabidv φ ι x A | ψ = ι x A | χ

Proof

Step Hyp Ref Expression
1 riotabidv.1 φ ψ χ
2 1 anbi2d φ x A ψ x A χ
3 2 iotabidv φ ι x | x A ψ = ι x | x A χ
4 df-riota ι x A | ψ = ι x | x A ψ
5 df-riota ι x A | χ = ι x | x A χ
6 3 4 5 3eqtr4g φ ι x A | ψ = ι x A | χ