Theorem difss 4066

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

Syntax hints:   ∖ cdif 3884   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  difssd  4067  difss2  4068  ssdifss  4070  0dif  4335  disj4  4392  difsnpss  4740  unidif  4875  iunxdif2  4983  difexg  5251  difelpw  5274  reldif  5725  cnvdif  6047  difxp  6067  frpoind  6245  wfiOLD  6254  tz7.7  6292  fresaun  6645  fresaunres2  6646  resdif  6737  fndmdif  6919  tfi  7700  peano5  7740  peano5OLD  7741  wfrlem16OLD  8155  oelim2  8426  swoer  8528  swoord1  8529  swoord2  8530  ralxpmap  8684  boxcutc  8729  undom  8846  undomOLD  8847  domunsncan  8859  sbthlem2  8871  sbthlem4  8873  sbthlem5  8874  limenpsi  8939  diffi  8962  php3  8995  phplem2OLD  9001  php3OLD  9007  frfi  9059  fofinf1o  9094  ixpfi2  9117  elfiun  9189  marypha1lem  9192  wemapso  9310  infdifsn  9415  cantnflem2  9448  frind  9508  frr1  9517  dfac8alem  9785  acnnum  9808  inffien  9819  kmlem5  9910  infdif  9965  infdif2  9966  ackbij1lem18  9993  fictb  10001  fin23lem7  10072  fin23lem11  10073  fin23lem28  10096  fin23lem30  10098  compsscnvlem  10126  isf34lem2  10129  compssiso  10130  isf34lem4  10133  fin1a2lem7  10162  axcclem  10213  zornn0g  10261  ttukey2g  10272  pinn  10634  niex  10637  ltsopi  10644  dmaddpi  10646  dmmulpi  10647  lerelxr  11038  mulnzcnopr  11621  dflt2  12882  expcl2lem  13794  expclzlem  13806  hashun2  14098  fsumss  15437  fsumless  15508  cvgcmpce  15530  fprodss  15658  rpnnen2lem9  15931  isstruct2  16850  structcnvcnv  16854  strleun  16858  strle1  16859  fsets  16870  mreexexlem2d  17354  gsumpropd2lem  18363  symgfixf1  19045  f1omvdmvd  19051  mvdco  19053  f1omvdconj  19054  pmtrfb  19073  pmtrfconj  19074  symggen  19078  symggen2  19079  psgnunilem1  19101  frgpnabllem2  19475  dprdss  19632  dprd2da  19645  dmdprdsplit2lem  19648  dpjidcl  19661  ablfac1b  19673  ablfac1eu  19676  isdrng2  20001  drngmcl  20004  drngid2  20007  isdrngd  20016  cntzsdrg  20070  subdrgint  20071  xrs1mnd  20636  xrs10  20637  xrs1cmn  20638  xrge0subm  20639  xrge0cmn  20640  cnmgpid  20660  cnmsubglem  20661  expghm  20697  dsmmfi  20945  islinds2  21020  lindsind2  21026  lindfrn  21028  islindf4  21045  mdetdiaglem  21747  mdetrsca2  21753  mdetrlin2  21756  mdetralt  21757  mdetunilem5  21765  mdetunilem9  21769  maducoeval2  21789  smadiadetglem1  21820  isopn2  22183  ntrval2  22202  ntrdif  22203  clsdif  22204  ntrss  22206  cmclsopn  22213  discld  22240  mretopd  22243  lpsscls  22292  restntr  22333  cmpcld  22553  2ndcsep  22610  1stccnp  22613  llycmpkgen2  22701  1stckgen  22705  txkgen  22803  qtopcld  22864  qtopcmap  22870  kqdisj  22883  isufil2  23059  ufileu  23070  filufint  23071  fixufil  23073  cfinufil  23079  ufilen  23081  fin1aufil  23083  supnfcls  23171  flimfnfcls  23179  alexsublem  23195  alexsubALTlem3  23200  cldsubg  23262  imasdsf1olem  23526  recld2  23977  sszcld  23980  xrge0gsumle  23996  divcn  24031  cdivcncf  24084  bcth3  24495  ismbl2  24691  cmmbl  24698  nulmbl  24699  nulmbl2  24700  unmbl  24701  voliunlem1  24714  voliunlem2  24715  ioombl1lem4  24725  ioombl1  24726  uniioombllem3  24749  mbfss  24810  itg1cl  24849  itg1ge0  24850  i1f0  24851  i1f1  24854  i1fmul  24860  itg1addlem4  24863  itg1addlem4OLD  24864  itg1mulc  24869  itg10a  24875  itg1ge0a  24876  itg1climres  24879  itg2cnlem1  24926  itgioo  24980  itgsplitioo  25002  limcdif  25040  ellimc2  25041  ellimc3  25043  limcflflem  25044  limcflf  25045  limcmo  25046  limcresi  25049  dvreslem  25073  dvres2lem  25074  dvidlem  25079  dvcnp2  25084  dvaddbr  25102  dvmulbr  25103  dvcobr  25110  dvrec  25119  dvcnvlem  25140  lhop1lem  25177  lhop  25180  tdeglem4  25224  tdeglem4OLD  25225  deg1n0ima  25254  aacjcl  25487  taylthlem2  25533  abelth  25600  logcnlem5  25801  dvlog2  25808  efopnlem2  25812  dvcncxp1  25896  dvcnsqrt  25897  cxpcn2  25899  sqrtcn  25903  efrlim  26119  jensen  26138  amgm  26140  lgamgulmlem2  26179  lgamucov  26187  wilthlem2  26218  dchrelbas2  26385  rpvmasum2  26660  dchrisum0re  26661  dchrisum0lem3  26667  dchrisum0  26668  tgisline  26988  upgrss  27458  frgrwopreg2  28683  difxp1ss  30870  difxp2ss  30871  xrge00  31295  symgcom2  31353  pmtrcnel  31358  pmtrcnel2  31359  pmtrcnelor  31360  cycpmrn  31410  tocyccntz  31411  submatres  31756  madjusmdetlem2  31778  madjusmdetlem3  31779  qtophaus  31786  fsumcvg4  31900  gsumesum  32027  pwsiga  32098  sigainb  32104  carsggect  32285  omsmeas  32290  sitgclg  32309  ballotlemfelz  32457  ballotlemfp1  32458  ballotth  32504  cxpcncf1  32575  logdivsqrle  32630  hgt750lemb  32636  kur14lem6  33173  kur14lem7  33174  cvmscld  33235  satfvsucsuc  33327  satfrnmapom  33332  mclsppslem  33545  fundmpss  33740  relsset  34190  limitssson  34213  fnsingle  34221  funimage  34230  cldbnd  34515  clsun  34517  topdifinffinlem  35518  inunissunidif  35546  pibt2  35588  matunitlindflem1  35773  poimirlem8  35785  poimirlem26  35803  poimirlem30  35807  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  voliunnfl  35821  cnambfre  35825  dvtan  35827  dvasin  35861  dvacos  35862  areacirclem4  35868  fdc  35903  divrngcl  36115  isdrngo2  36116  isdrngo3  36117  islsati  37008  hdmap14lem2a  39881  prjspreln0  40448  prjspvs  40449  prjspeclsp  40451  0prjspnrel  40464  istopclsd  40522  diophin  40594  dnnumch1  40869  isdomn3  41029  deg1mhm  41032  gneispace  41744  inaex  41915  sumnnodd  43171  cncficcgt0  43429  cncfiooicclem1  43434  cxpcncf2  43440  dirkercncflem2  43645  fourierdlem62  43709  fourierdlem66  43713  fourierdlem68  43715  fourierdlem95  43742  etransclem24  43799  etransclem44  43819  gsumge0cl  43909  sge0fodjrnlem  43954  carageniuncllem1  44059  smfresal  44322  lindslinindimp2lem2  45800  iscnrm3rlem2  46235  amgmlemALT  46507