Theorem difss 4131

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

Syntax hints:   ∖ cdif 3945   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  difssd  4132  difss2  4133  ssdifss  4135  0dif  4401  disj4  4458  difsnpss  4810  unidif  4946  iunxdif2  5056  difexg  5327  difelpw  5351  reldif  5815  cnvdif  6143  difxp  6163  frpoind  6343  wfiOLD  6352  tz7.7  6390  fresaun  6762  fresaunres2  6763  resdif  6854  fndmdif  7043  tfi  7844  peano5  7886  peano5OLD  7887  wfrlem16OLD  8326  oelim2  8597  swoer  8735  swoord1  8736  swoord2  8737  ralxpmap  8892  boxcutc  8937  undom  9061  undomOLD  9062  domunsncan  9074  sbthlem2  9086  sbthlem4  9088  sbthlem5  9089  limenpsi  9154  diffi  9181  php3  9214  phplem2OLD  9220  php3OLD  9226  frfi  9290  fofinf1o  9329  ixpfi2  9352  elfiun  9427  marypha1lem  9430  wemapso  9548  infdifsn  9654  cantnflem2  9687  frind  9747  frr1  9756  dfac8alem  10026  acnnum  10049  inffien  10060  kmlem5  10151  infdif  10206  infdif2  10207  ackbij1lem18  10234  fictb  10242  fin23lem7  10313  fin23lem11  10314  fin23lem28  10337  fin23lem30  10339  compsscnvlem  10367  isf34lem2  10370  compssiso  10371  isf34lem4  10374  fin1a2lem7  10403  axcclem  10454  zornn0g  10502  ttukey2g  10513  pinn  10875  niex  10878  ltsopi  10885  dmaddpi  10887  dmmulpi  10888  lerelxr  11281  mulnzcnopr  11864  dflt2  13131  expcl2lem  14043  expclzlem  14053  hashun2  14347  fsumss  15675  fsumless  15746  cvgcmpce  15768  fprodss  15896  rpnnen2lem9  16169  isstruct2  17086  structcnvcnv  17090  strleun  17094  strle1  17095  fsets  17106  mreexexlem2d  17593  gsumpropd2lem  18604  symgfixf1  19346  f1omvdmvd  19352  mvdco  19354  f1omvdconj  19355  pmtrfb  19374  pmtrfconj  19375  symggen  19379  symggen2  19380  psgnunilem1  19402  frgpnabllem2  19783  dprdss  19940  dprd2da  19953  dmdprdsplit2lem  19956  dpjidcl  19969  ablfac1b  19981  ablfac1eu  19984  isdrng2  20514  drngmcl  20517  drngid2  20521  isdrngd  20533  isdrngdOLD  20535  cntzsdrg  20561  subdrgint  20562  xrs1mnd  21183  xrs10  21184  xrs1cmn  21185  xrge0subm  21186  xrge0cmn  21187  cnmgpid  21207  cnmsubglem  21208  expghm  21246  dsmmfi  21512  islinds2  21587  lindsind2  21593  lindfrn  21595  islindf4  21612  mdetdiaglem  22320  mdetrsca2  22326  mdetrlin2  22329  mdetralt  22330  mdetunilem5  22338  mdetunilem9  22342  maducoeval2  22362  smadiadetglem1  22393  isopn2  22756  ntrval2  22775  ntrdif  22776  clsdif  22777  ntrss  22779  cmclsopn  22786  discld  22813  mretopd  22816  lpsscls  22865  restntr  22906  cmpcld  23126  2ndcsep  23183  1stccnp  23186  llycmpkgen2  23274  1stckgen  23278  txkgen  23376  qtopcld  23437  qtopcmap  23443  kqdisj  23456  isufil2  23632  ufileu  23643  filufint  23644  fixufil  23646  cfinufil  23652  ufilen  23654  fin1aufil  23656  supnfcls  23744  flimfnfcls  23752  alexsublem  23768  alexsubALTlem3  23773  cldsubg  23835  imasdsf1olem  24099  recld2  24550  sszcld  24553  xrge0gsumle  24569  divcnOLD  24604  divcn  24606  cdivcncf  24661  bcth3  25072  ismbl2  25268  cmmbl  25275  nulmbl  25276  nulmbl2  25277  unmbl  25278  voliunlem1  25291  voliunlem2  25292  ioombl1lem4  25302  ioombl1  25303  uniioombllem3  25326  mbfss  25387  itg1cl  25426  itg1ge0  25427  i1f0  25428  i1f1  25431  i1fmul  25437  itg1addlem4  25440  itg1addlem4OLD  25441  itg1mulc  25446  itg10a  25452  itg1ge0a  25453  itg1climres  25456  itg2cnlem1  25503  itgioo  25557  itgsplitioo  25579  limcdif  25617  ellimc2  25618  ellimc3  25620  limcflflem  25621  limcflf  25622  limcmo  25623  limcresi  25626  dvreslem  25650  dvres2lem  25651  dvidlem  25656  dvcnp2  25661  dvaddbr  25679  dvmulbr  25680  dvcobr  25687  dvrec  25696  dvcnvlem  25717  lhop1lem  25754  lhop  25757  tdeglem4  25801  tdeglem4OLD  25802  deg1n0ima  25831  aacjcl  26064  taylthlem2  26110  abelth  26177  logcnlem5  26378  dvlog2  26385  efopnlem2  26389  dvcncxp1  26475  dvcnsqrt  26476  cxpcn2  26478  sqrtcn  26482  efrlim  26698  jensen  26717  amgm  26719  lgamgulmlem2  26758  lgamucov  26766  wilthlem2  26797  dchrelbas2  26964  rpvmasum2  27239  dchrisum0re  27240  dchrisum0lem3  27246  dchrisum0  27247  nnssn0s  27925  tgisline  28133  upgrss  28603  frgrwopreg2  29827  difxp1ss  32015  difxp2ss  32016  xrge00  32442  symgcom2  32503  pmtrcnel  32508  pmtrcnel2  32509  pmtrcnelor  32510  cycpmrn  32560  tocyccntz  32561  submatres  33072  madjusmdetlem2  33094  madjusmdetlem3  33095  qtophaus  33102  fsumcvg4  33216  gsumesum  33343  pwsiga  33414  sigainb  33420  carsggect  33603  omsmeas  33608  sitgclg  33627  ballotlemfelz  33775  ballotlemfp1  33776  ballotth  33822  cxpcncf1  33893  logdivsqrle  33948  hgt750lemb  33954  kur14lem6  34488  kur14lem7  34489  cvmscld  34550  satfvsucsuc  34642  satfrnmapom  34647  mclsppslem  34860  fundmpss  35030  relsset  35152  limitssson  35175  fnsingle  35183  funimage  35192  gg-dvcnp2  35460  gg-dvmulbr  35461  gg-dvcobr  35462  cldbnd  35514  clsun  35516  topdifinffinlem  36531  inunissunidif  36559  pibt2  36601  matunitlindflem1  36787  poimirlem8  36799  poimirlem26  36817  poimirlem30  36821  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  voliunnfl  36835  cnambfre  36839  dvtan  36841  dvasin  36875  dvacos  36876  areacirclem4  36882  fdc  36916  divrngcl  37128  isdrngo2  37129  isdrngo3  37130  islsati  38167  hdmap14lem2a  41041  prjspreln0  41653  prjspvs  41654  prjspeclsp  41656  0prjspnrel  41671  istopclsd  41740  diophin  41812  dnnumch1  42088  isdomn3  42248  deg1mhm  42251  gneispace  43187  inaex  43358  sumnnodd  44645  cncficcgt0  44903  cncfiooicclem1  44908  cxpcncf2  44914  dirkercncflem2  45119  fourierdlem62  45183  fourierdlem66  45187  fourierdlem68  45189  fourierdlem95  45216  etransclem24  45273  etransclem44  45293  gsumge0cl  45386  sge0fodjrnlem  45431  carageniuncllem1  45536  smfresal  45803  lindslinindimp2lem2  47228  iscnrm3rlem2  47662  amgmlemALT  47938