Theorem ssdif 3570

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 3428	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 568	. . 3 |- ( A C_ B -> ( ( x e. A /\ -. x e. C ) -> ( x e. B /\ -. x e. C ) ) )
3		eldif 3416	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3416	. . 3 |- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
5	2, 3, 4	3imtr4g 274	. 2 |- ( A C_ B -> ( x e. ( A \ C ) -> x e. ( B \ C ) ) )
6	5	ssrdv 3440	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   e. wcel 1889   \ cdif 3403   C_ wss 3406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-dif 3409  df-in 3413  df-ss 3420

This theorem is referenced by:  ssdifd  3571  php  7761  pssnn  7795  fin1a2lem13  8847  axcclem  8892  isercolllem3  13742  mvdco  17098  dprdres  17673  dpjidcl  17703  ablfac1eulem  17717  lspsnat  18380  lbsextlem2  18394  lbsextlem3  18395  mplmonmul  18700  cnsubdrglem  19031  clscon  20457  2ndcdisj2  20484  kqdisj  20759  nulmbl2  22502  i1f1  22660  itg11  22661  itg1climres  22684  limcresi  22852  dvreslem  22876  dvres2lem  22877  dvaddbr  22904  dvmulbr  22905  lhop  22980  elqaa  23290  difres  28223  imadifxp  28224  xrge00  28460  eulerpartlemmf  29220  eulerpartlemgf  29224  bj-2upln1upl  31630  mblfinlem3  31991  mblfinlem4  31992  ismblfin  31993  cnambfre  32001  divrngidl  32273  cntzsdrg  36080  radcnvrat  36674  fourierdlem62  38042