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	⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Proof of Theorem difss

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:   ∖ cdif 3118   ⊆ 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  5598  swoer  6537  swoord1  6538  swoord2  6539  phplem2  6827  phpm  6839  unfiin  6899  sbthlem2  6931  sbthlemi4  6933  sbthlemi5  6934  difinfinf  7074  pinn  7258  niex  7261  dmaddpi  7274  dmmulpi  7275  lerelxr  7969  fisumss  11342  fprodssdc  11540  structcnvcnv  12419  strleund  12493  strleun  12494  strle1g  12495  discld  12889  exmid1stab  13993