Theorem ssdif 3638

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

Assertion

Ref	Expression
ssdif

Proof of Theorem ssdif

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3497	. . . 4
2	1	anim1d 564	. . 3
3		eldif 3485	. . 3
4		eldif 3485	. . 3
5	2, 3, 4	3imtr4g 270	. 2
6	5	ssrdv 3509	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  e.wcel 1818  \cdif 3472  C_wss 3475

This theorem is referenced by:  ssdifd  3639  php  7721  pssnn  7758  mapfienOLD  8159  fin1a2lem13  8813  axcclem  8858  isercolllem3  13489  mvdco  16470  dprdres  17075  dpjidcl  17107  dpjidclOLD  17114  ablfac1eulem  17123  lspsnat  17791  lbsextlem2  17805  lbsextlem3  17806  mplmonmul  18126  cnsubdrglem  18469  clscon  19931  2ndcdisj2  19958  kqdisj  20233  nulmbl2  21947  i1f1  22097  itg11  22098  itg1climres  22121  limcresi  22289  dvreslem  22313  dvres2lem  22314  dvaddbr  22341  dvmulbr  22342  lhop  22417  elqaa  22718  difres  27457  imadifxp  27458  xrge00  27674  eulerpartlemmf  28314  eulerpartlemgf  28318  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  cnambfre  30063  divrngidl  30425  cntzsdrg  31151  radcnvrat  31195  fourierdlem62  31951  bj-2upln1upl  34582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489