Theorem riotaeqdv

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

	Ref	Expression
Hypothesis	riotaeqdv.1	$$⊢\phi \to A=B$$
Assertion	riotaeqdv	$$⊢\phi \to \left(\iota x\in A|\psi \right)=\left(\iota x\in B|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaeqdv.1	$$⊢\phi \to A=B$$
2	1	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in B\right)$$
3	2	anbi1d	$$⊢\phi \to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \psi \right)\right)$$
4	3	iotabidv	$$⊢\phi \to \left(\iota x|\left(x\in A\wedge \psi \right)\right)=\left(\iota x|\left(x\in B\wedge \psi \right)\right)$$
5		df-riota	$$⊢\left(\iota x\in A|\psi \right)=\left(\iota x|\left(x\in A\wedge \psi \right)\right)$$
6		df-riota	$$⊢\left(\iota x\in B|\psi \right)=\left(\iota x|\left(x\in B\wedge \psi \right)\right)$$
7	4 5 6	3eqtr4g	$$⊢\phi \to \left(\iota x\in A|\psi \right)=\left(\iota x\in B|\psi \right)$$