Theorem ssdif 3486

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

Assertion

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

Proof of Theorem ssdif

Dummy variable x is distinct from all other variables.

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1756   \ cdif 3320   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326  df-in 3330  df-ss 3337

This theorem is referenced by:  ssdifd  3487  php  7487  pssnn  7523  mapfienOLD  7919  fin1a2lem13  8573  axcclem  8618  isercolllem3  13136  mvdco  15942  dprdres  16513  dpjidcl  16545  dpjidclOLD  16552  ablfac1eulem  16561  lspsnat  17203  lbsextlem2  17217  lbsextlem3  17218  mplmonmul  17520  cnsubdrglem  17839  clscon  19009  2ndcdisj2  19036  kqdisj  19280  nulmbl2  20993  i1f1  21143  itg11  21144  itg1climres  21167  limcresi  21335  dvreslem  21359  dvres2lem  21360  dvaddbr  21387  dvmulbr  21388  lhop  21463  elqaa  21763  imadifxp  25890  xrge00  26098  eulerpartlemmf  26710  eulerpartlemgf  26714  mblfinlem3  28383  mblfinlem4  28384  ismblfin  28385  cnambfre  28393  divrngidl  28781  cntzsdrg  29512  bj-2upln1upl  32364