Theorem difss 2219

Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
difss	|- (A \ B) (_ A

Proof of Theorem difss

Step	Hyp	Ref	Expression
1		eldifi 2214	. 2 |- (x e. (A \ B) -> x e. A)
2	1	ssriv 2121	1 |- (A \ B) (_ A

Syntax hints:   \ cdif 2096   (_ wss 2099

This theorem is referenced by:  ssdifss 2220  disj4 2370  0dif 2389  inundif 2395  difsn 2528  unidif 2597  iunxdif2 2666  difexg 2796  tz7.7 3001  tfi 3207  peano5 3241  reldif 3353  resdif 3816  oelim2 4358  undom 4579  sbthlem1 4592  sbthlem2 4593  sbthlem4 4595  sbthlem5 4596  limenpsi 4652  phplem2 4656  phplem4 4658  php 4660  php3 4662  pssnn 4681  unfi 4697  inf3lem3 4760  kmlem5 4915  numthlem 4929  pinn 5160  niex 5163  dmaddpi 5172  dmmulpi 5173  mulnzcnopr 5854  seq1rn 6687  acdc2lem2 7701  acdc5lem2 7704  ruclem13 7734  infxpidmlem11 7774  infdif 7780  infdif2 7781  isopn2 7883  iincld 7889  clsval2 7895  ntrval2 7896  ntrss 7898  cmclsopn 7903  cmntrcld 7904  lpval 7953  lpsscls 7955  islp2 7957  lpbl 8090  bcthlem14 8223  twpar2 10773  ranleqt 10793  finfin 10798  islp3 11011  cnfilca 11088  rcfpfillem6 11094  rcfpfil 11095  dtopcl 11107  ntrcmp 11458  clscmp 11459  cldbnd 11462  clsun 11465  subntr 11482  cptclsscpt 11489  hscptsscld 11491  alexsublem3 11498  connsub 11502  ist1-2 11603  isnrm2 11613  isufil2 11650  ufileulem 11657  ufileu 11658  filufint 11659  fixufil 11661  ufilen 11664  fcluscf 11724  flimfnfcls 11727  difxp 11798  fimax 11837  indexf 11847  hmeocld 11961  recms 12066

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-dif 2101  df-in 2103  df-ss 2105

Copyright terms: Public domain