Theorem riotabidv

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

	Ref	Expression
Hypothesis	riotabidv.1	$$⊢\phi \to \left(\psi \leftrightarrow \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 \leftrightarrow \chi \right)$$
2	1	anbi2d	$$⊢\phi \to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \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)$$