Theorem difss 4128

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

Syntax hints:   ∖ cdif 3941   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-ss 3961

This theorem is referenced by:  difssd  4129  difss2  4130  ssdifss  4132  0dif  4403  disj4  4460  difsnpss  4812  unidif  4946  iunxdif2  5057  difexg  5330  difelpw  5353  reldif  5817  cnvdif  6150  difxp  6170  frpoind  6350  wfiOLD  6359  tz7.7  6397  fresaun  6768  fresaunres2  6769  resdif  6859  fndmdif  7050  tfi  7858  peano5  7900  peano5OLD  7901  wfrlem16OLD  8345  oelim2  8616  swoer  8755  swoord1  8756  swoord2  8757  ralxpmap  8915  boxcutc  8960  undom  9087  undomOLD  9088  domunsncan  9100  sbthlem2  9112  sbthlem4  9114  sbthlem5  9115  limenpsi  9180  diffi  9207  php3  9240  phplem2OLD  9246  php3OLD  9252  frfi  9316  fofinf1o  9358  ixpfi2  9381  elfiun  9460  marypha1lem  9463  wemapso  9581  infdifsn  9687  cantnflem2  9720  frind  9780  frr1  9789  dfac8alem  10059  acnnum  10082  inffien  10093  kmlem5  10184  infdif  10239  infdif2  10240  ackbij1lem18  10267  fictb  10275  fin23lem7  10346  fin23lem11  10347  fin23lem28  10370  fin23lem30  10372  compsscnvlem  10400  isf34lem2  10403  compssiso  10404  isf34lem4  10407  fin1a2lem7  10436  axcclem  10487  zornn0g  10535  ttukey2g  10546  pinn  10908  niex  10911  ltsopi  10918  dmaddpi  10920  dmmulpi  10921  lerelxr  11314  mulnzcnf  11897  dflt2  13167  expcl2lem  14079  expclzlem  14089  hashun2  14383  fsumss  15712  fsumless  15783  cvgcmpce  15805  fprodss  15933  rpnnen2lem9  16207  isstruct2  17126  structcnvcnv  17130  strleun  17134  strle1  17135  fsets  17146  mreexexlem2d  17633  gsumpropd2lem  18647  symgfixf1  19409  f1omvdmvd  19415  mvdco  19417  f1omvdconj  19418  pmtrfb  19437  pmtrfconj  19438  symggen  19442  symggen2  19443  psgnunilem1  19465  frgpnabllem2  19846  dprdss  20003  dprd2da  20016  dmdprdsplit2lem  20019  dpjidcl  20032  ablfac1b  20044  ablfac1eu  20047  isdrng2  20655  drngmcl  20658  drngid2  20662  isdrngd  20674  isdrngdOLD  20676  cntzsdrg  20707  subdrgint  20708  isdomn3  21270  xrs1mnd  21359  xrs10  21360  xrs1cmn  21361  xrge0subm  21362  xrge0cmn  21363  cnmgpid  21384  cnmsubglem  21385  expghm  21423  dsmmfi  21694  islinds2  21769  lindsind2  21775  lindfrn  21777  islindf4  21794  psdmul  22118  mdetdiaglem  22549  mdetrsca2  22555  mdetrlin2  22558  mdetralt  22559  mdetunilem5  22567  mdetunilem9  22571  maducoeval2  22591  smadiadetglem1  22622  isopn2  22985  ntrval2  23004  ntrdif  23005  clsdif  23006  ntrss  23008  cmclsopn  23015  discld  23042  mretopd  23045  lpsscls  23094  restntr  23135  cmpcld  23355  2ndcsep  23412  1stccnp  23415  llycmpkgen2  23503  1stckgen  23507  txkgen  23605  qtopcld  23666  qtopcmap  23672  kqdisj  23685  isufil2  23861  ufileu  23872  filufint  23873  fixufil  23875  cfinufil  23881  ufilen  23883  fin1aufil  23885  supnfcls  23973  flimfnfcls  23981  alexsublem  23997  alexsubALTlem3  24002  cldsubg  24064  imasdsf1olem  24328  recld2  24779  sszcld  24782  xrge0gsumle  24798  divcnOLD  24833  divcn  24835  cdivcncf  24890  bcth3  25308  ismbl2  25505  cmmbl  25512  nulmbl  25513  nulmbl2  25514  unmbl  25515  voliunlem1  25528  voliunlem2  25529  ioombl1lem4  25539  ioombl1  25540  uniioombllem3  25563  mbfss  25624  itg1cl  25663  itg1ge0  25664  i1f0  25665  i1f1  25668  i1fmul  25674  itg1addlem4  25677  itg1addlem4OLD  25678  itg1mulc  25683  itg10a  25689  itg1ge0a  25690  itg1climres  25693  itg2cnlem1  25740  itgioo  25794  itgsplitioo  25816  limcdif  25854  ellimc2  25855  ellimc3  25857  limcflflem  25858  limcflf  25859  limcmo  25860  limcresi  25863  dvreslem  25887  dvres2lem  25888  dvidlem  25893  dvcnp2  25898  dvcnp2OLD  25899  dvaddbr  25917  dvmulbr  25918  dvmulbrOLD  25919  dvcobr  25926  dvcobrOLD  25927  dvrec  25936  dvcnvlem  25957  lhop1lem  25995  lhop  25998  tdeglem4  26044  tdeglem4OLD  26045  deg1n0ima  26074  aacjcl  26312  taylthlem2  26359  taylthlem2OLD  26360  abelth  26428  logcnlem5  26630  dvlog2  26637  efopnlem2  26641  dvcncxp1  26727  dvcnsqrt  26728  cxpcn2  26731  sqrtcn  26735  efrlim  26951  efrlimOLD  26952  jensen  26971  amgm  26973  lgamgulmlem2  27012  lgamucov  27020  wilthlem2  27051  dchrelbas2  27220  rpvmasum2  27495  dchrisum0re  27496  dchrisum0lem3  27502  dchrisum0  27503  nnssn0s  28248  tgisline  28508  upgrss  28978  frgrwopreg2  30206  difxp1ss  32403  difxp2ss  32404  xrge00  32836  symgcom2  32902  pmtrcnel  32907  pmtrcnel2  32908  pmtrcnelor  32909  cycpmrn  32961  tocyccntz  32962  submatres  33540  madjusmdetlem2  33562  madjusmdetlem3  33563  qtophaus  33570  fsumcvg4  33684  gsumesum  33811  pwsiga  33882  sigainb  33888  carsggect  34071  omsmeas  34076  sitgclg  34095  ballotlemfelz  34243  ballotlemfp1  34244  ballotth  34290  cxpcncf1  34360  logdivsqrle  34415  hgt750lemb  34421  kur14lem6  34954  kur14lem7  34955  cvmscld  35016  satfvsucsuc  35108  satfrnmapom  35113  mclsppslem  35326  fundmpss  35495  relsset  35617  limitssson  35640  fnsingle  35648  funimage  35657  cldbnd  35943  clsun  35945  topdifinffinlem  36959  inunissunidif  36987  pibt2  37029  matunitlindflem1  37222  poimirlem8  37234  poimirlem26  37252  poimirlem30  37256  mblfinlem3  37265  mblfinlem4  37266  ismblfin  37267  voliunnfl  37270  cnambfre  37274  dvtan  37276  dvasin  37310  dvacos  37311  areacirclem4  37317  fdc  37351  divrngcl  37563  isdrngo2  37564  isdrngo3  37565  islsati  38598  hdmap14lem2a  41472  prjspreln0  42170  prjspvs  42171  prjspeclsp  42173  0prjspnrel  42188  istopclsd  42264  diophin  42336  dnnumch1  42612  deg1mhm  42772  gneispace  43708  inaex  43878  sumnnodd  45158  cncficcgt0  45416  cncfiooicclem1  45421  cxpcncf2  45427  dirkercncflem2  45632  fourierdlem62  45696  fourierdlem66  45700  fourierdlem68  45702  fourierdlem95  45729  etransclem24  45786  etransclem44  45806  gsumge0cl  45899  sge0fodjrnlem  45944  carageniuncllem1  46049  smfresal  46316  dfnbgrss  47326  dfnbgrss2  47333  lindslinindimp2lem2  47715  iscnrm3rlem2  48148  amgmlemALT  48424