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  3486  undif1ss  3489  undifabs  3491  inundifss  3492  undifss  3495  unidif  3828  iunxdif2  3921  difexg  4130  reldif  4731  cnvdif  5017  resdif  5464  fndmdif  5601  swoer  6541  swoord1  6542  swoord2  6543  phplem2  6831  phpm  6843  unfiin  6903  sbthlem2  6935  sbthlemi4  6937  sbthlemi5  6938  difinfinf  7078  pinn  7271  niex  7274  dmaddpi  7287  dmmulpi  7288  lerelxr  7982  fisumss  11355  fprodssdc  11553  structcnvcnv  12432  strleund  12506  strleun  12507  strle1g  12508  discld  12930  exmid1stab  14033