Theorem reuabaiotaiota

Description: The iota and the alternate iota over a wff ph are equal iff there is a unique satisfying value of { x | ph } = { y } . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	reuabaiotaiota	$$⊢\exists !y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left(\iota x|\phi \right)=\iota$$

Proof

Step	Hyp	Ref	Expression
1		uniintab	$$⊢\exists !y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
2		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
3		df-aiota	$$⊢\iota =\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
4	2 3	eqeq12i	$$⊢\left(\iota x|\phi \right)=\iota \leftrightarrow \bigcup \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}=\bigcap \left\{y|\left\{x|\phi \right\}=\left\{y\right\}\right\}$$
5	1 4	bitr4i	$$⊢\exists !y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left(\iota x|\phi \right)=\iota$$