Theorem dfiota2

Description: Alternate definition for descriptions. Definition 8.18 in Quine p. 56. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	dfiota2	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
2		absn	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=y\right)$$
3	2	abbii	$$⊢\left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$
4	3	unieqi	$$⊢\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\bigcup \left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$
5	1 4	eqtri	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$