Theorem aiotaint

Description: This is to df-aiota what iotauni is to df-iota (it uses intersection like df-aiota , similar to iotauni using union like df-iota ; we could also prove an analogous result using union here too, in the same way that we have iotaint ). (Contributed by BJ, 31-Aug-2024)

	Ref	Expression
Assertion	aiotaint	$$⊢\exists !x\phi \to \iota =\bigcap \left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		reuaiotaiota	$$⊢\exists !x\phi \leftrightarrow \left(\iota x|\phi \right)=\iota$$
2	1	biimpi	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)=\iota$$
3		iotaint	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)=\bigcap \left\{x|\phi \right\}$$
4	2 3	eqtr3d	$$⊢\exists !x\phi \to \iota =\bigcap \left\{x|\phi \right\}$$