Theorem iotabi

Description: Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	iotabi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abbi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left\{x|\phi \right\}=\left\{x|\psi \right\}$$
2	1	eqeq1d	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \left\{x|\psi \right\}=\left\{z\right\}\right)$$
3	2	abbidv	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}=\left\{z|\left\{x|\psi \right\}=\left\{z\right\}\right\}$$
4	3	unieqd	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \bigcup \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}=\bigcup \left\{z|\left\{x|\psi \right\}=\left\{z\right\}\right\}$$
5		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{z|\left\{x|\phi \right\}=\left\{z\right\}\right\}$$
6		df-iota	$$⊢\left(\iota x|\psi \right)=\bigcup \left\{z|\left\{x|\psi \right\}=\left\{z\right\}\right\}$$
7	4 5 6	3eqtr4g	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(\iota x|\phi \right)=\left(\iota x|\psi \right)$$