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

Metamath Proof Explorer

Theorem ssundif

Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion ssundif 
|- ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )

Proof

Step Hyp Ref Expression
1 pm5.6 
 |-  ( ( ( x e. A /\ -. x e. B ) -> x e. C ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
2 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3 2 imbi1i 
 |-  ( ( x e. ( A \ B ) -> x e. C ) <-> ( ( x e. A /\ -. x e. B ) -> x e. C ) )
4 elun 
 |-  ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) )
5 4 imbi2i 
 |-  ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. A -> ( x e. B \/ x e. C ) ) )
6 1 3 5 3bitr4ri 
 |-  ( ( x e. A -> x e. ( B u. C ) ) <-> ( x e. ( A \ B ) -> x e. C ) )
7 6 albii 
 |-  ( A. x ( x e. A -> x e. ( B u. C ) ) <-> A. x ( x e. ( A \ B ) -> x e. C ) )
8 df-ss 
 |-  ( A C_ ( B u. C ) <-> A. x ( x e. A -> x e. ( B u. C ) ) )
9 df-ss 
 |-  ( ( A \ B ) C_ C <-> A. x ( x e. ( A \ B ) -> x e. C ) )
10 7 8 9 3bitr4i 
 |-  ( A C_ ( B u. C ) <-> ( A \ B ) C_ C )