Theorem difss 3303

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 3299	. 2 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) → 𝑥 ∈ 𝐴)
2	1	ssriv 3201	1 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴

Syntax hints:   ∖ cdif 3167   ⊆ wss 3170

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-in 3176  df-ss 3183

This theorem is referenced by:  difssd  3304  difss2  3305  ssdifss  3307  0dif  3536  undif1ss  3539  undifabs  3541  inundifss  3542  undifss  3545  unidif  3887  iunxdif2  3981  difexg  4192  exmid1stab  4259  reldif  4802  cnvdif  5097  resdif  5555  fndmdif  5697  swoer  6660  swoord1  6661  swoord2  6662  phplem2  6964  phpm  6976  unfiin  7037  sbthlem2  7074  sbthlemi4  7076  sbthlemi5  7077  difinfinf  7217  pinn  7437  niex  7440  dmaddpi  7453  dmmulpi  7454  lerelxr  8150  fisumss  11773  fprodssdc  11971  structcnvcnv  12918  strleund  13005  strleun  13006  strle1g  13008  discld  14678