Theorem ssdif 3598

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 3457	. . . 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 3445	. . 3 |- ( x e. ( A \ C ) <-> ( x e. A /\ -. x e. C ) )
4		eldif 3445	. . 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 3469	1 |- ( A C_ B -> ( A \ C ) C_ ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   e. wcel 1758   \ cdif 3432   C_ wss 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-dif 3438  df-in 3442  df-ss 3449

This theorem is referenced by:  ssdifd  3599  php  7604  pssnn  7641  mapfienOLD  8037  fin1a2lem13  8691  axcclem  8736  isercolllem3  13261  mvdco  16069  dprdres  16646  dpjidcl  16678  dpjidclOLD  16685  ablfac1eulem  16694  lspsnat  17348  lbsextlem2  17362  lbsextlem3  17363  mplmonmul  17666  cnsubdrglem  17988  clscon  19165  2ndcdisj2  19192  kqdisj  19436  nulmbl2  21150  i1f1  21300  itg11  21301  itg1climres  21324  limcresi  21492  dvreslem  21516  dvres2lem  21517  dvaddbr  21544  dvmulbr  21545  lhop  21620  elqaa  21920  imadifxp  26089  xrge00  26291  eulerpartlemmf  26901  eulerpartlemgf  26905  mblfinlem3  28577  mblfinlem4  28578  ismblfin  28579  cnambfre  28587  divrngidl  28975  cntzsdrg  29706  bj-2upln1upl  32834