Theorem difss 3095

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 3091	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 2974	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 2939   C_ wss 2942

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-dif 2945  df-in 2949  df-ss 2956

This theorem is referenced by:  difssd  3096  difss2  3097  ssdifss  3099  0dif  3320  undif1ss  3323  undifabs  3325  inundifss  3326  undifss  3328  difsnpssim  3532  unidif  3637  iunxdif2  3730  difexg  3923  reldif  4482  cnvdif  4755  resdif  5173  fndmdif  5297  swoer  6162  swoord1  6163  swoord2  6164  phplem2  6344  phpm  6355  pinn  6435  niex  6438  dmaddpi  6451  dmmulpi  6452  lerelxr  7111