This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )