Theorem difss 3331

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

Assertion

Ref	Expression
difss	⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Proof of Theorem difss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3327	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3229	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3195   ⊆ wss 3198

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-dif 3200  df-in 3204  df-ss 3211

This theorem is referenced by:  difssd  3332  difss2  3333  ssdifss  3335  0dif  3564  undif1ss  3567  undifabs  3569  inundifss  3570  undifss  3573  unidif  3923  iunxdif2  4017  difexg  4229  exmid1stab  4296  reldif  4845  cnvdif  5141  resdif  5602  fndmdif  5748  swoer  6725  swoord1  6726  swoord2  6727  phplem2  7034  phpm  7047  unfiin  7111  sbthlem2  7148  sbthlemi4  7150  sbthlemi5  7151  difinfinf  7291  pinn  7519  niex  7522  dmaddpi  7535  dmmulpi  7536  lerelxr  8232  fisumss  11943  fprodssdc  12141  structcnvcnv  13088  strleund  13176  strleun  13177  strle1g  13179  discld  14850