Theorem unissint

Description: If the union of a class is included in its intersection, the class is either the empty set or a singleton ( uniintsn ). (Contributed by NM, 30-Oct-2010) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	unissint	|- ( U. A C_ |^| A <-> ( A = (/) \/ U. A = |^| A ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( U. A C_ |^| A /\ -. A = (/) ) -> U. A C_ |^| A )
2		df-ne	|- ( A =/= (/) <-> -. A = (/) )
3		intssuni	|- ( A =/= (/) -> |^| A C_ U. A )
4	2 3	sylbir	|- ( -. A = (/) -> |^| A C_ U. A )
5	4	adantl	|- ( ( U. A C_ |^| A /\ -. A = (/) ) -> |^| A C_ U. A )
6	1 5	eqssd	|- ( ( U. A C_ |^| A /\ -. A = (/) ) -> U. A = |^| A )
7	6	ex	|- ( U. A C_ |^| A -> ( -. A = (/) -> U. A = |^| A ) )
8	7	orrd	|- ( U. A C_ |^| A -> ( A = (/) \/ U. A = |^| A ) )
9		ssv	|- U. A C_ _V
10		int0	|- |^| (/) = _V
11	9 10	sseqtrri	|- U. A C_ |^| (/)
12		inteq	|- ( A = (/) -> |^| A = |^| (/) )
13	11 12	sseqtrrid	|- ( A = (/) -> U. A C_ |^| A )
14		eqimss	|- ( U. A = |^| A -> U. A C_ |^| A )
15	13 14	jaoi	|- ( ( A = (/) \/ U. A = |^| A ) -> U. A C_ |^| A )
16	8 15	impbii	|- ( U. A C_ |^| A <-> ( A = (/) \/ U. A = |^| A ) )