Theorem difss 4130

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

Syntax hints:   ∖ cdif 3944   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  difssd  4131  difss2  4132  ssdifss  4134  0dif  4400  disj4  4457  difsnpss  4809  unidif  4945  iunxdif2  5055  difexg  5326  difelpw  5350  reldif  5813  cnvdif  6140  difxp  6160  frpoind  6340  wfiOLD  6349  tz7.7  6387  fresaun  6759  fresaunres2  6760  resdif  6851  fndmdif  7039  tfi  7837  peano5  7879  peano5OLD  7880  wfrlem16OLD  8319  oelim2  8591  swoer  8729  swoord1  8730  swoord2  8731  ralxpmap  8886  boxcutc  8931  undom  9055  undomOLD  9056  domunsncan  9068  sbthlem2  9080  sbthlem4  9082  sbthlem5  9083  limenpsi  9148  diffi  9175  php3  9208  phplem2OLD  9214  php3OLD  9220  frfi  9284  fofinf1o  9323  ixpfi2  9346  elfiun  9421  marypha1lem  9424  wemapso  9542  infdifsn  9648  cantnflem2  9681  frind  9741  frr1  9750  dfac8alem  10020  acnnum  10043  inffien  10054  kmlem5  10145  infdif  10200  infdif2  10201  ackbij1lem18  10228  fictb  10236  fin23lem7  10307  fin23lem11  10308  fin23lem28  10331  fin23lem30  10333  compsscnvlem  10361  isf34lem2  10364  compssiso  10365  isf34lem4  10368  fin1a2lem7  10397  axcclem  10448  zornn0g  10496  ttukey2g  10507  pinn  10869  niex  10872  ltsopi  10879  dmaddpi  10881  dmmulpi  10882  lerelxr  11273  mulnzcnopr  11856  dflt2  13123  expcl2lem  14035  expclzlem  14045  hashun2  14339  fsumss  15667  fsumless  15738  cvgcmpce  15760  fprodss  15888  rpnnen2lem9  16161  isstruct2  17078  structcnvcnv  17082  strleun  17086  strle1  17087  fsets  17098  mreexexlem2d  17585  gsumpropd2lem  18594  symgfixf1  19298  f1omvdmvd  19304  mvdco  19306  f1omvdconj  19307  pmtrfb  19326  pmtrfconj  19327  symggen  19331  symggen2  19332  psgnunilem1  19354  frgpnabllem2  19734  dprdss  19891  dprd2da  19904  dmdprdsplit2lem  19907  dpjidcl  19920  ablfac1b  19932  ablfac1eu  19935  isdrng2  20317  drngmcl  20320  drngid2  20324  isdrngd  20336  isdrngdOLD  20338  cntzsdrg  20406  subdrgint  20407  xrs1mnd  20968  xrs10  20969  xrs1cmn  20970  xrge0subm  20971  xrge0cmn  20972  cnmgpid  20992  cnmsubglem  20993  expghm  21029  dsmmfi  21277  islinds2  21352  lindsind2  21358  lindfrn  21360  islindf4  21377  mdetdiaglem  22082  mdetrsca2  22088  mdetrlin2  22091  mdetralt  22092  mdetunilem5  22100  mdetunilem9  22104  maducoeval2  22124  smadiadetglem1  22155  isopn2  22518  ntrval2  22537  ntrdif  22538  clsdif  22539  ntrss  22541  cmclsopn  22548  discld  22575  mretopd  22578  lpsscls  22627  restntr  22668  cmpcld  22888  2ndcsep  22945  1stccnp  22948  llycmpkgen2  23036  1stckgen  23040  txkgen  23138  qtopcld  23199  qtopcmap  23205  kqdisj  23218  isufil2  23394  ufileu  23405  filufint  23406  fixufil  23408  cfinufil  23414  ufilen  23416  fin1aufil  23418  supnfcls  23506  flimfnfcls  23514  alexsublem  23530  alexsubALTlem3  23535  cldsubg  23597  imasdsf1olem  23861  recld2  24312  sszcld  24315  xrge0gsumle  24331  divcn  24366  cdivcncf  24419  bcth3  24830  ismbl2  25026  cmmbl  25033  nulmbl  25034  nulmbl2  25035  unmbl  25036  voliunlem1  25049  voliunlem2  25050  ioombl1lem4  25060  ioombl1  25061  uniioombllem3  25084  mbfss  25145  itg1cl  25184  itg1ge0  25185  i1f0  25186  i1f1  25189  i1fmul  25195  itg1addlem4  25198  itg1addlem4OLD  25199  itg1mulc  25204  itg10a  25210  itg1ge0a  25211  itg1climres  25214  itg2cnlem1  25261  itgioo  25315  itgsplitioo  25337  limcdif  25375  ellimc2  25376  ellimc3  25378  limcflflem  25379  limcflf  25380  limcmo  25381  limcresi  25384  dvreslem  25408  dvres2lem  25409  dvidlem  25414  dvcnp2  25419  dvaddbr  25437  dvmulbr  25438  dvcobr  25445  dvrec  25454  dvcnvlem  25475  lhop1lem  25512  lhop  25515  tdeglem4  25559  tdeglem4OLD  25560  deg1n0ima  25589  aacjcl  25822  taylthlem2  25868  abelth  25935  logcnlem5  26136  dvlog2  26143  efopnlem2  26147  dvcncxp1  26231  dvcnsqrt  26232  cxpcn2  26234  sqrtcn  26238  efrlim  26454  jensen  26473  amgm  26475  lgamgulmlem2  26514  lgamucov  26522  wilthlem2  26553  dchrelbas2  26720  rpvmasum2  26995  dchrisum0re  26996  dchrisum0lem3  27002  dchrisum0  27003  tgisline  27858  upgrss  28328  frgrwopreg2  29552  difxp1ss  31738  difxp2ss  31739  xrge00  32165  symgcom2  32223  pmtrcnel  32228  pmtrcnel2  32229  pmtrcnelor  32230  cycpmrn  32280  tocyccntz  32281  submatres  32724  madjusmdetlem2  32746  madjusmdetlem3  32747  qtophaus  32754  fsumcvg4  32868  gsumesum  32995  pwsiga  33066  sigainb  33072  carsggect  33255  omsmeas  33260  sitgclg  33279  ballotlemfelz  33427  ballotlemfp1  33428  ballotth  33474  cxpcncf1  33545  logdivsqrle  33600  hgt750lemb  33606  kur14lem6  34140  kur14lem7  34141  cvmscld  34202  satfvsucsuc  34294  satfrnmapom  34299  mclsppslem  34512  fundmpss  34676  relsset  34798  limitssson  34821  fnsingle  34829  funimage  34838  gg-divcn  35101  gg-dvcnp2  35112  gg-dvmulbr  35113  gg-dvcobr  35114  cldbnd  35149  clsun  35151  topdifinffinlem  36166  inunissunidif  36194  pibt2  36236  matunitlindflem1  36422  poimirlem8  36434  poimirlem26  36452  poimirlem30  36456  mblfinlem3  36465  mblfinlem4  36466  ismblfin  36467  voliunnfl  36470  cnambfre  36474  dvtan  36476  dvasin  36510  dvacos  36511  areacirclem4  36517  fdc  36551  divrngcl  36763  isdrngo2  36764  isdrngo3  36765  islsati  37802  hdmap14lem2a  40676  prjspreln0  41295  prjspvs  41296  prjspeclsp  41298  0prjspnrel  41313  istopclsd  41371  diophin  41443  dnnumch1  41719  isdomn3  41879  deg1mhm  41882  gneispace  42818  inaex  42989  sumnnodd  44281  cncficcgt0  44539  cncfiooicclem1  44544  cxpcncf2  44550  dirkercncflem2  44755  fourierdlem62  44819  fourierdlem66  44823  fourierdlem68  44825  fourierdlem95  44852  etransclem24  44909  etransclem44  44929  gsumge0cl  45022  sge0fodjrnlem  45067  carageniuncllem1  45172  smfresal  45439  lindslinindimp2lem2  47042  iscnrm3rlem2  47476  amgmlemALT  47752