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	|- ( E! x ph <-> U. { x | ph } = |^| { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		euabsn2	|- ( E! x ph <-> E. y { x | ph } = { y } )
2		uniintsn	|- ( U. { x | ph } = |^| { x | ph } <-> E. y { x | ph } = { y } )
3	1 2	bitr4i	|- ( E! x ph <-> U. { x | ph } = |^| { x | ph } )