Theorem aiotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	aiotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \iota =y$$

Proof

Step	Hyp	Ref	Expression
1		eusnsn	$$⊢\exists !z\left\{z\right\}=\left\{y\right\}$$
2		eqcom	$$⊢\left\{y\right\}=\left\{z\right\}\leftrightarrow \left\{z\right\}=\left\{y\right\}$$
3	2	eubii	$$⊢\exists !z\left\{y\right\}=\left\{z\right\}\leftrightarrow \exists !z\left\{z\right\}=\left\{y\right\}$$
4	1 3	mpbir	$$⊢\exists !z\left\{y\right\}=\left\{z\right\}$$
5		eqeq1	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \left\{y\right\}=\left\{z\right\}\right)$$
6	5	eubidv	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\exists !z\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \exists !z\left\{y\right\}=\left\{z\right\}\right)$$
7	4 6	mpbiri	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \exists !z\left\{x|\phi \right\}=\left\{z\right\}$$
8		absn	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow x=y\right)$$
9		reuabaiotaiota	$$⊢\exists !z\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \left(\iota x|\phi \right)=\iota$$
10		eqcom	$$⊢\left(\iota x|\phi \right)=\iota \leftrightarrow \iota =\left(\iota x|\phi \right)$$
11	9 10	bitri	$$⊢\exists !z\left\{x|\phi \right\}=\left\{z\right\}\leftrightarrow \iota =\left(\iota x|\phi \right)$$
12	7 8 11	3imtr3i	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \iota =\left(\iota x|\phi \right)$$
13		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
14	12 13	eqtrd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \iota =y$$