Theorem intssuni

Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006)

	Ref	Expression
Assertion	intssuni	|- ( A =/= (/) -> |^| A C_ U. A )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	|- ( ( A =/= (/) /\ A. y e. A x e. y ) -> E. y e. A x e. y )
2	1	ex	|- ( A =/= (/) -> ( A. y e. A x e. y -> E. y e. A x e. y ) )
3		vex	|- x e. _V
4	3	elint2	|- ( x e. |^| A <-> A. y e. A x e. y )
5		eluni2	|- ( x e. U. A <-> E. y e. A x e. y )
6	2 4 5	3imtr4g	|- ( A =/= (/) -> ( x e. |^| A -> x e. U. A ) )
7	6	ssrdv	|- ( A =/= (/) -> |^| A C_ U. A )