Theorem difss 2167

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 2162	. 2 |- (x e. (A \ B) -> x e. A)
2	1	ssriv 2069	1 |- (A \ B) (_ A

Syntax hints:   \ cdif 2044   (_ wss 2047

This theorem is referenced by:  ssdifss 2168  disj4 2317  0dif 2336  difsn 2464  unidif 2530  iunxdif2 2598  difexg 2722  tz7.7 2973  tfi 3126  peano5 3153  reldif 3264  oelim2 4222  undom 4438  sbthlem1 4447  sbthlem2 4448  sbthlem4 4450  sbthlem5 4451  limenpsi 4505  phplem2 4509  phplem4 4511  php 4513  php3 4515  php3OLD 4516  pssnn 4534  unfi 4551  unfiOLD 4552  inf3lem3 4615  kmlem5 4769  numthlem 4783  pinn 5006  niex 5009  dmaddpi 5018  dmmulpi 5019  mulnzcnopr 5702  seq1rn 6322  acdc2lem2 7489  acdc5lem2 7492  ruclem13 7522  infxpidmlem11 7562  infdif 7568  infdif2 7569  isopn2 7673  iincld 7679  clsval2 7685  ntrval2 7686  ntrss 7688  cmclsopn 7693  cmntrcld 7694  lpval 7743  lpsscls 7745  islp2 7747  lpbl 7880  bcthlem14 8012  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598  dtopcl 10615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-dif 2049  df-in 2051  df-ss 2053

Copyright terms: Public domain