Theorem ssdif 3479

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 3338	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 559	. . 3 |- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif 3326	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3326	. . 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 3350	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1755   \ cdif 3313   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330

This theorem is referenced by:  ssdifd  3480  php  7483  pssnn  7519  mapfienOLD  7915  fin1a2lem13  8569  axcclem  8614  isercolllem3  13128  mvdco  15931  dprdres  16499  dpjidcl  16531  dpjidclOLD  16538  ablfac1eulem  16547  lspsnat  17148  lbsextlem2  17162  lbsextlem3  17163  mplmonmul  17477  cnsubdrglem  17708  clscon  18876  2ndcdisj2  18903  kqdisj  19147  nulmbl2  20860  i1f1  21010  itg11  21011  itg1climres  21034  limcresi  21202  dvreslem  21226  dvres2lem  21227  dvaddbr  21254  dvmulbr  21255  lhop  21330  elqaa  21673  imadifxp  25763  xrge00  25970  eulerpartlemmf  26606  eulerpartlemgf  26610  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  cnambfre  28284  divrngidl  28672  cntzsdrg  29404  bj-2upln1upl  32121