Theorem difss 4068

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

Syntax hints:   ∖ cdif 3881   ⊆ wss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3887  df-ss 3901

This theorem is referenced by:  difssd  4069  difss2  4070  ssdifss  4072  0dif  4335  disj4  4389  difsnpss  4742  unidif  4875  iunxdif2  4985  difexg  5259  difelpw  5284  reldif  5760  cnvdif  6096  difxp  6118  frpoind  6296  tz7.7  6339  fresaun  6701  fresaunres2  6702  resdif  6791  fndmdif  6986  tfi  7796  peano5  7837  oelim2  8525  swoer  8669  swoord1  8670  swoord2  8671  ralxpmap  8838  boxcutc  8883  undom  8997  domunsncan  9009  sbthlem2  9020  sbthlem4  9022  sbthlem5  9023  limenpsi  9084  diffi  9103  php3  9137  frfi  9189  fofinf1o  9236  ixpfi2  9254  elfiun  9337  marypha1lem  9340  wemapso  9460  infdifsn  9573  cantnflem2  9606  frind  9669  frr1  9678  dfac8alem  9946  acnnum  9969  inffien  9980  kmlem5  10072  infdif  10125  infdif2  10126  ackbij1lem18  10153  fictb  10161  fin23lem7  10234  fin23lem11  10235  fin23lem28  10258  fin23lem30  10260  compsscnvlem  10288  isf34lem2  10291  compssiso  10292  isf34lem4  10295  fin1a2lem7  10324  axcclem  10375  zornn0g  10423  ttukey2g  10434  pinn  10797  niex  10800  ltsopi  10807  dmaddpi  10809  dmmulpi  10810  lerelxr  11204  mulnzcnf  11792  dflt2  13094  expcl2lem  14030  expclzlem  14040  hashun2  14340  fsumss  15682  fsumless  15754  cvgcmpce  15776  fprodss  15908  rpnnen2lem9  16184  isstruct2  17114  structcnvcnv  17118  strleun  17122  strle1  17123  fsets  17134  mreexexlem2d  17606  gsumpropd2lem  18642  symgfixf1  19406  f1omvdmvd  19412  mvdco  19414  f1omvdconj  19415  pmtrfb  19434  pmtrfconj  19435  symggen  19439  symggen2  19440  psgnunilem1  19462  frgpnabllem2  19843  dprdss  20000  dprd2da  20013  dmdprdsplit2lem  20016  dpjidcl  20029  ablfac1b  20041  ablfac1eu  20044  isdomn3  20690  isdrng2  20718  drngmclOLD  20726  drngid2  20727  isdrngd  20740  isdrngdOLD  20742  cntzsdrg  20777  subdrgint  20778  cnmgpid  21407  cnmsubglem  21408  xrs1mnd  21418  xrs10  21419  xrs1cmn  21420  xrge0subm  21421  xrge0cmn  21422  expghm  21453  dsmmfi  21716  islinds2  21791  lindsind2  21797  lindfrn  21799  islindf4  21816  psdmul  22157  mdetdiaglem  22584  mdetrsca2  22590  mdetrlin2  22593  mdetralt  22594  mdetunilem5  22602  mdetunilem9  22606  maducoeval2  22626  smadiadetglem1  22657  isopn2  23018  ntrval2  23037  ntrdif  23038  clsdif  23039  ntrss  23041  cmclsopn  23048  discld  23075  mretopd  23078  lpsscls  23127  restntr  23168  cmpcld  23388  2ndcsep  23445  1stccnp  23448  llycmpkgen2  23536  1stckgen  23540  txkgen  23638  qtopcld  23699  qtopcmap  23705  kqdisj  23718  isufil2  23894  ufileu  23905  filufint  23906  fixufil  23908  cfinufil  23914  ufilen  23916  fin1aufil  23918  supnfcls  24006  flimfnfcls  24014  alexsublem  24030  alexsubALTlem3  24035  cldsubg  24097  imasdsf1olem  24359  recld2  24801  sszcld  24804  xrge0gsumle  24820  divcn  24856  cdivcncf  24909  bcth3  25319  ismbl2  25515  cmmbl  25522  nulmbl  25523  nulmbl2  25524  unmbl  25525  voliunlem1  25538  voliunlem2  25539  ioombl1lem4  25549  ioombl1  25550  uniioombllem3  25573  mbfss  25634  itg1cl  25673  itg1ge0  25674  i1f0  25675  i1f1  25678  i1fmul  25684  itg1addlem4  25687  itg1mulc  25692  itg10a  25698  itg1ge0a  25699  itg1climres  25702  itg2cnlem1  25749  itgioo  25804  itgsplitioo  25826  limcdif  25864  ellimc2  25865  ellimc3  25867  limcflflem  25868  limcflf  25869  limcmo  25870  limcresi  25873  dvreslem  25897  dvres2lem  25898  dvidlem  25903  dvcnp2  25908  dvaddbr  25926  dvmulbr  25927  dvcobr  25934  dvrec  25943  dvcnvlem  25964  lhop1lem  26001  lhop  26004  tdeglem4  26046  deg1n0ima  26075  aacjcl  26314  taylthlem2  26360  abelth  26427  logcnlem5  26631  dvlog2  26638  efopnlem2  26642  dvcncxp1  26728  dvcnsqrt  26729  cxpcn2  26731  sqrtcn  26735  efrlim  26954  jensen  26973  amgm  26975  lgamgulmlem2  27014  lgamucov  27022  wilthlem2  27053  dchrelbas2  27221  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem3  27503  dchrisum0  27504  nnssn0s  28333  tgisline  28715  upgrss  29177  frgrwopreg2  30409  difxp1ss  32612  difxp2ss  32613  xrge00  33095  symgcom2  33167  pmtrcnel  33172  pmtrcnel2  33173  pmtrcnelor  33174  cycpmrn  33226  tocyccntz  33227  evlextv  33736  vietalem  33773  submatres  34000  madjusmdetlem2  34022  madjusmdetlem3  34023  qtophaus  34030  fsumcvg4  34144  gsumesum  34253  pwsiga  34324  sigainb  34330  carsggect  34512  omsmeas  34517  sitgclg  34536  ballotlemfelz  34685  ballotlemfp1  34686  ballotth  34732  cxpcncf1  34789  logdivsqrle  34844  hgt750lemb  34850  fineqvnttrclse  35318  kur14lem6  35452  kur14lem7  35453  cvmscld  35514  satfvsucsuc  35606  satfrnmapom  35611  mclsppslem  35824  fundmpss  36008  relsset  36127  limitssson  36150  fnsingle  36158  funimage  36167  cldbnd  36567  clsun  36569  topdifinffinlem  37722  inunissunidif  37750  pibt2  37792  matunitlindflem1  37996  poimirlem8  38008  poimirlem26  38026  poimirlem30  38030  mblfinlem3  38039  mblfinlem4  38040  ismblfin  38041  voliunnfl  38044  cnambfre  38048  dvtan  38050  dvasin  38084  dvacos  38085  areacirclem4  38091  fdc  38125  divrngcl  38337  isdrngo2  38338  isdrngo3  38339  islsati  39499  hdmap14lem2a  42372  redvmptabs  42850  prjspreln0  43072  prjspvs  43073  prjspeclsp  43075  0prjspnrel  43090  istopclsd  43162  diophin  43234  dnnumch1  43502  deg1mhm  43658  gneispace  44591  inaex  44754  sumnnodd  46087  cncficcgt0  46343  cncfiooicclem1  46348  cxpcncf2  46354  dirkercncflem2  46559  fourierdlem62  46623  fourierdlem66  46627  fourierdlem68  46629  fourierdlem95  46656  etransclem24  46713  etransclem44  46733  gsumge0cl  46826  sge0fodjrnlem  46871  carageniuncllem1  46976  smfresal  47243  dfnbgrss  48355  dfnbgrss2  48362  lindslinindimp2lem2  48962  iscnrm3rlem2  49443  amgmlemALT  50305