Theorem uniintab

Description: The union and the intersection of a class abstraction are equal exactly when there is a unique satisfying value of ph ( x ) . (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	uniintab	$$⊢\exists !x\phi \leftrightarrow \bigcup \left\{x|\phi \right\}=\bigcap \left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		euabsn2	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
2		uniintsn	$$⊢\bigcup \left\{x|\phi \right\}=\bigcap \left\{x|\phi \right\}\leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
3	1 2	bitr4i	$$⊢\exists !x\phi \leftrightarrow \bigcup \left\{x|\phi \right\}=\bigcap \left\{x|\phi \right\}$$