Theorem difss 2163

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

Syntax hints:   \ cdif 2040   (_ wss 2043

This theorem is referenced by:  ssdifss 2164  disj4 2313  0dif 2332  difsn 2460  unidif 2525  iunxdif2 2593  difexg 2717  tz7.7 2968  tfi 3121  peano5 3148  reldif 3259  oelim2 4212  undom 4424  sbthlem1 4433  sbthlem2 4434  sbthlem4 4436  sbthlem5 4437  limenpsi 4491  phplem2 4495  phplem4 4497  php 4499  php3 4501  pssnn 4519  unfi 4534  inf3lem3 4595  kmlem5 4749  numthlem 4763  pinn 4986  niex 4989  dmaddpi 4998  dmmulpi 4999  mulnzcnopr 5679  seq1rn 6267  acdc2lem2 7439  acdc5lem2 7442  ruclem13 7473  infxpidmlem11 7513  infdif 7519  infdif2 7520  isopn2 7623  iincld 7629  clsval2 7635  ntrval2 7636  ntrss 7638  cmclsopn 7643  cmntrcld 7644  lpval 7693  lpsscls 7695  islp2 7697  lpbl 7832  bcthlem14 7962  cnfilca 10487  dtopcl 10495

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049

Copyright terms: Public domain