Theorem difss 3335

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

Syntax hints:   ∖ cdif 3198   ⊆ wss 3201

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-in 3207  df-ss 3214

This theorem is referenced by:  difssd  3336  difss2  3337  ssdifss  3339  0dif  3568  undif1ss  3571  undifabs  3573  inundifss  3574  undifss  3577  unidif  3930  iunxdif2  4024  difexg  4236  exmid1stab  4304  reldif  4853  cnvdif  5150  resdif  5614  fndmdif  5761  swoer  6773  swoord1  6774  swoord2  6775  phplem2  7082  phpm  7095  unfiin  7161  sbthlem2  7200  sbthlemi4  7202  sbthlemi5  7203  difinfinf  7343  pinn  7572  niex  7575  dmaddpi  7588  dmmulpi  7589  lerelxr  8284  fisumss  12016  fprodssdc  12214  structcnvcnv  13161  strleund  13249  strleun  13250  strle1g  13252  discld  14930