# Metamath Proof Explorer

## Theorem riotabidv

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

Ref Expression
Hypothesis riotabidv.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion riotabidv ${⊢}{\phi }\to \left(\iota {x}\in {A}|{\psi }\right)=\left(\iota {x}\in {A}|{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 riotabidv.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 1 anbi2d ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {\psi }\right)↔\left({x}\in {A}\wedge {\chi }\right)\right)$
3 2 iotabidv ${⊢}{\phi }\to \left(\iota {x}|\left({x}\in {A}\wedge {\psi }\right)\right)=\left(\iota {x}|\left({x}\in {A}\wedge {\chi }\right)\right)$
4 df-riota ${⊢}\left(\iota {x}\in {A}|{\psi }\right)=\left(\iota {x}|\left({x}\in {A}\wedge {\psi }\right)\right)$
5 df-riota ${⊢}\left(\iota {x}\in {A}|{\chi }\right)=\left(\iota {x}|\left({x}\in {A}\wedge {\chi }\right)\right)$
6 3 4 5 3eqtr4g ${⊢}{\phi }\to \left(\iota {x}\in {A}|{\psi }\right)=\left(\iota {x}\in {A}|{\chi }\right)$