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		dfss2	|- ( A C_ ( B u. C ) <-> A. x ( x e. A -> x e. ( B u. C ) ) )
9		dfss2	|- ( ( 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 )