Theorem ssdif 3745

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 3597	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 588	. . 3 |- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif 3584	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3584	. . 3 |- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
5	2, 3, 4	3imtr4g 285	. 2 |- ( A C_ B -> ( x e. ( A \ C ) -> x e. ( B \ C ) ) )
6	5	ssrdv 3609	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   e. wcel 1990   \ cdif 3571   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  ssdifd  3746  php  8144  pssnn  8178  fin1a2lem13  9234  axcclem  9279  isercolllem3  14397  mvdco  17865  dprdres  18427  dpjidcl  18457  ablfac1eulem  18471  lspsnat  19145  lbsextlem2  19159  lbsextlem3  19160  mplmonmul  19464  cnsubdrglem  19797  clsconn  21233  2ndcdisj2  21260  kqdisj  21535  nulmbl2  23304  i1f1  23457  itg11  23458  itg1climres  23481  limcresi  23649  dvreslem  23673  dvres2lem  23674  dvaddbr  23701  dvmulbr  23702  lhop  23779  elqaa  24077  difres  29413  imadifxp  29414  xrge00  29686  eulerpartlemmf  30437  eulerpartlemgf  30441  bj-2upln1upl  33012  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  cnambfre  33458  divrngidl  33827  cntzsdrg  37772  radcnvrat  38513  fourierdlem62  40385