Theorem difss 4062

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

Syntax hints:   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  difssd  4063  difss2  4064  ssdifss  4066  0dif  4332  disj4  4389  difsnpss  4737  unidif  4872  iunxdif2  4979  difexg  5246  difelpw  5269  reldif  5714  cnvdif  6036  difxp  6056  frpoind  6230  wfiOLD  6239  tz7.7  6277  fresaun  6629  fresaunres2  6630  resdif  6720  fndmdif  6901  tfi  7675  peano5  7714  peano5OLD  7715  wfrlem16OLD  8126  oelim2  8388  swoer  8486  swoord1  8487  swoord2  8488  ralxpmap  8642  boxcutc  8687  undom  8800  domunsncan  8812  sbthlem2  8824  sbthlem4  8826  sbthlem5  8827  limenpsi  8888  phplem2  8893  php3  8899  diffi  8979  frfi  8989  fofinf1o  9024  ixpfi2  9047  elfiun  9119  marypha1lem  9122  wemapso  9240  infdifsn  9345  cantnflem2  9378  frind  9439  frr1  9448  dfac8alem  9716  acnnum  9739  inffien  9750  kmlem5  9841  infdif  9896  infdif2  9897  ackbij1lem18  9924  fictb  9932  fin23lem7  10003  fin23lem11  10004  fin23lem28  10027  fin23lem30  10029  compsscnvlem  10057  isf34lem2  10060  compssiso  10061  isf34lem4  10064  fin1a2lem7  10093  axcclem  10144  zornn0g  10192  ttukey2g  10203  pinn  10565  niex  10568  ltsopi  10575  dmaddpi  10577  dmmulpi  10578  lerelxr  10969  mulnzcnopr  11551  dflt2  12811  expcl2lem  13722  expclzlem  13734  hashun2  14026  fsumss  15365  fsumless  15436  cvgcmpce  15458  fprodss  15586  rpnnen2lem9  15859  isstruct2  16778  structcnvcnv  16782  strleun  16786  strle1  16787  fsets  16798  mreexexlem2d  17271  gsumpropd2lem  18278  symgfixf1  18960  f1omvdmvd  18966  mvdco  18968  f1omvdconj  18969  pmtrfb  18988  pmtrfconj  18989  symggen  18993  symggen2  18994  psgnunilem1  19016  frgpnabllem2  19390  dprdss  19547  dprd2da  19560  dmdprdsplit2lem  19563  dpjidcl  19576  ablfac1b  19588  ablfac1eu  19591  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  cntzsdrg  19985  subdrgint  19986  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  xrge0subm  20551  xrge0cmn  20552  cnmgpid  20572  cnmsubglem  20573  expghm  20609  dsmmfi  20855  islinds2  20930  lindsind2  20936  lindfrn  20938  islindf4  20955  mdetdiaglem  21655  mdetrsca2  21661  mdetrlin2  21664  mdetralt  21665  mdetunilem5  21673  mdetunilem9  21677  maducoeval2  21697  smadiadetglem1  21728  isopn2  22091  ntrval2  22110  ntrdif  22111  clsdif  22112  ntrss  22114  cmclsopn  22121  discld  22148  mretopd  22151  lpsscls  22200  restntr  22241  cmpcld  22461  2ndcsep  22518  1stccnp  22521  llycmpkgen2  22609  1stckgen  22613  txkgen  22711  qtopcld  22772  qtopcmap  22778  kqdisj  22791  isufil2  22967  ufileu  22978  filufint  22979  fixufil  22981  cfinufil  22987  ufilen  22989  fin1aufil  22991  supnfcls  23079  flimfnfcls  23087  alexsublem  23103  alexsubALTlem3  23108  cldsubg  23170  imasdsf1olem  23434  recld2  23883  sszcld  23886  xrge0gsumle  23902  divcn  23937  cdivcncf  23990  bcth3  24400  ismbl2  24596  cmmbl  24603  nulmbl  24604  nulmbl2  24605  unmbl  24606  voliunlem1  24619  voliunlem2  24620  ioombl1lem4  24630  ioombl1  24631  uniioombllem3  24654  mbfss  24715  itg1cl  24754  itg1ge0  24755  i1f0  24756  i1f1  24759  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  itg1mulc  24774  itg10a  24780  itg1ge0a  24781  itg1climres  24784  itg2cnlem1  24831  itgioo  24885  itgsplitioo  24907  limcdif  24945  ellimc2  24946  ellimc3  24948  limcflflem  24949  limcflf  24950  limcmo  24951  limcresi  24954  dvreslem  24978  dvres2lem  24979  dvidlem  24984  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvrec  25024  dvcnvlem  25045  lhop1lem  25082  lhop  25085  tdeglem4  25129  tdeglem4OLD  25130  deg1n0ima  25159  aacjcl  25392  taylthlem2  25438  abelth  25505  logcnlem5  25706  dvlog2  25713  efopnlem2  25717  dvcncxp1  25801  dvcnsqrt  25802  cxpcn2  25804  sqrtcn  25808  efrlim  26024  jensen  26043  amgm  26045  lgamgulmlem2  26084  lgamucov  26092  wilthlem2  26123  dchrelbas2  26290  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem3  26572  dchrisum0  26573  tgisline  26892  upgrss  27361  frgrwopreg2  28584  difxp1ss  30771  difxp2ss  30772  xrge00  31197  symgcom2  31255  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  cycpmrn  31312  tocyccntz  31313  submatres  31658  madjusmdetlem2  31680  madjusmdetlem3  31681  qtophaus  31688  fsumcvg4  31802  gsumesum  31927  pwsiga  31998  sigainb  32004  carsggect  32185  omsmeas  32190  sitgclg  32209  ballotlemfelz  32357  ballotlemfp1  32358  ballotth  32404  cxpcncf1  32475  logdivsqrle  32530  hgt750lemb  32536  kur14lem6  33073  kur14lem7  33074  cvmscld  33135  satfvsucsuc  33227  satfrnmapom  33232  mclsppslem  33445  fundmpss  33646  relsset  34117  limitssson  34140  fnsingle  34148  funimage  34157  cldbnd  34442  clsun  34444  topdifinffinlem  35445  inunissunidif  35473  pibt2  35515  matunitlindflem1  35700  poimirlem8  35712  poimirlem26  35730  poimirlem30  35734  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  voliunnfl  35748  cnambfre  35752  dvtan  35754  dvasin  35788  dvacos  35789  areacirclem4  35795  fdc  35830  divrngcl  36042  isdrngo2  36043  isdrngo3  36044  islsati  36935  hdmap14lem2a  39808  prjspreln0  40369  prjspvs  40370  prjspeclsp  40372  0prjspnrel  40385  istopclsd  40438  diophin  40510  dnnumch1  40785  isdomn3  40945  deg1mhm  40948  gneispace  41633  inaex  41804  sumnnodd  43061  cncficcgt0  43319  cncfiooicclem1  43324  cxpcncf2  43330  dirkercncflem2  43535  fourierdlem62  43599  fourierdlem66  43603  fourierdlem68  43605  fourierdlem95  43632  etransclem24  43689  etransclem44  43709  gsumge0cl  43799  sge0fodjrnlem  43844  carageniuncllem1  43949  smfresal  44209  lindslinindimp2lem2  45688  iscnrm3rlem2  46123  amgmlemALT  46393