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

Metamath Proof Explorer

Theorem intssuni2

Description: Subclass relationship for intersection and union. (Contributed by NM, 29-Jul-2006)

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

Proof

Step Hyp Ref Expression
1 intssuni 
 |-  ( A =/= (/) -> |^| A C_ U. A )
2 uniss 
 |-  ( A C_ B -> U. A C_ U. B )
3 1 2 sylan9ssr 
 |-  ( ( A C_ B /\ A =/= (/) ) -> |^| A C_ U. B )