Theorem difss 3261

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

Syntax hints:   \ cdif 3126   C_ wss 3129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-dif 3131  df-in 3135  df-ss 3142

This theorem is referenced by:  difssd  3262  difss2  3263  ssdifss  3265  0dif  3494  undif1ss  3497  undifabs  3499  inundifss  3500  undifss  3503  unidif  3840  iunxdif2  3933  difexg  4142  exmid1stab  4206  reldif  4744  cnvdif  5032  resdif  5480  fndmdif  5618  swoer  6558  swoord1  6559  swoord2  6560  phplem2  6848  phpm  6860  unfiin  6920  sbthlem2  6952  sbthlemi4  6954  sbthlemi5  6955  difinfinf  7095  pinn  7303  niex  7306  dmaddpi  7319  dmmulpi  7320  lerelxr  8014  fisumss  11391  fprodssdc  11589  structcnvcnv  12468  strleund  12552  strleun  12553  strle1g  12555  discld  13418