Theorem ssdif

Description: Difference law for subsets. (Contributed by NM, 28-May-1998)

	Ref	Expression
Assertion	ssdif	|- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d	|- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif	|- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif	|- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
5	2 3 4	3imtr4g	|- ( A C_ B -> ( x e. ( A \ C ) -> x e. ( B \ C ) ) )
6	5	ssrdv	|- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )