Theorem difss 3141

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

Syntax hints:   ∖ cdif 3010   ⊆ wss 3013

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-dif 3015  df-in 3019  df-ss 3026

This theorem is referenced by:  difssd  3142  difss2  3143  ssdifss  3145  0dif  3373  undif1ss  3376  undifabs  3378  inundifss  3379  undifss  3382  unidif  3707  iunxdif2  3800  difexg  4001  reldif  4587  cnvdif  4871  resdif  5310  fndmdif  5443  swoer  6360  swoord1  6361  swoord2  6362  phplem2  6649  phpm  6661  unfiin  6716  sbthlem2  6747  sbthlemi4  6749  sbthlemi5  6750  pinn  6965  niex  6968  dmaddpi  6981  dmmulpi  6982  lerelxr  7646  fisumss  10935  structcnvcnv  11659  strleund  11731  strleun  11732  strle1g  11733  discld  11988