Theorem difss 3253

Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)

Assertion

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

Proof of Theorem difss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3249	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 3151	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 3118   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-in 3127  df-ss 3134

This theorem is referenced by:  difssd  3254  difss2  3255  ssdifss  3257  0dif  3485  undif1ss  3488  undifabs  3490  inundifss  3491  undifss  3494  unidif  3826  iunxdif2  3919  difexg  4128  reldif  4729  cnvdif  5015  resdif  5462  fndmdif  5599  swoer  6539  swoord1  6540  swoord2  6541  phplem2  6829  phpm  6841  unfiin  6901  sbthlem2  6933  sbthlemi4  6935  sbthlemi5  6936  difinfinf  7076  pinn  7264  niex  7267  dmaddpi  7280  dmmulpi  7281  lerelxr  7975  fisumss  11348  fprodssdc  11546  structcnvcnv  12425  strleund  12499  strleun  12500  strle1g  12501  discld  12895  exmid1stab  13998