Theorem dfaiota2

Description: Alternate definition of the alternate version of Russell's definition of a description binder. Definition 8.18 in Quine p. 56. (Contributed by AV, 24-Aug-2022)

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

Proof

Step	Hyp	Ref	Expression
1		df-aiota	$$⊢\iota =\bigcap \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	inteqi	$$⊢\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\bigcap \left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$
5	1 4	eqtri	$$⊢\iota =\bigcap \left\{y|\forall x\left(\phi \leftrightarrow x=y\right)\right\}$$