Theorem riotaeqbidv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Hypotheses	riotaeqbidv.1	$$⊢\phi \to A=B$$
	riotaeqbidv.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	riotaeqbidv	$$⊢\phi \to \left(\iota x\in A|\psi \right)=\left(\iota x\in B|\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaeqbidv.1	$$⊢\phi \to A=B$$
2		riotaeqbidv.2	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
3	2	riotabidv	$$⊢\phi \to \left(\iota x\in A|\psi \right)=\left(\iota x\in A|\chi \right)$$
4	1	riotaeqdv	$$⊢\phi \to \left(\iota x\in A|\chi \right)=\left(\iota x\in B|\chi \right)$$
5	3 4	eqtrd	$$⊢\phi \to \left(\iota x\in A|\psi \right)=\left(\iota x\in B|\chi \right)$$