Theorem difss 1596

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

Syntax hints:   \ cdif 1484   (_ wss 1487

This theorem is referenced by:  difexg 1703  disj4 1737  0dif 1757  unidif 1943  tz7.7 2224  tfi 2244  peano5 2394  reldif 2492  undom 3342  sbthlem1 3349  sbthlem2 3350  sbthlem4 3352  sbthlem5 3353  limenpsi 3400  phplem3 3405  phplem5 3407  php 3409  php3 3411  pssnn 3428  unblem1 3431  unfi 3441  inf3lem3 3466  kmlem5 3584  kmlem10 3589  numthlem 3598  pinn 3800  niex 3803  dmaddpi 3812  dmmulpi 3813  seqrn2 4674  ruclem13 4897  infxpidmlem11 4943  infdif 4948

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-in 1491  df-ss 1492

metamath.org