Theorem difss 4089

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

Syntax hints:   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-ss 3922

This theorem is referenced by:  difssd  4090  difss2  4091  ssdifss  4093  0dif  4358  disj4  4412  difsnpss  4761  unidif  4895  iunxdif2  5005  difexg  5271  difelpw  5296  reldif  5762  cnvdif  6096  difxp  6117  frpoind  6294  tz7.7  6337  fresaun  6699  fresaunres2  6700  resdif  6789  fndmdif  6980  tfi  7793  peano5  7833  oelim2  8520  swoer  8663  swoord1  8664  swoord2  8665  ralxpmap  8830  boxcutc  8875  undom  8989  domunsncan  9001  sbthlem2  9012  sbthlem4  9014  sbthlem5  9015  limenpsi  9076  diffi  9099  php3  9133  frfi  9190  fofinf1o  9241  ixpfi2  9259  elfiun  9339  marypha1lem  9342  wemapso  9462  infdifsn  9572  cantnflem2  9605  frind  9665  frr1  9674  dfac8alem  9942  acnnum  9965  inffien  9976  kmlem5  10068  infdif  10121  infdif2  10122  ackbij1lem18  10149  fictb  10157  fin23lem7  10229  fin23lem11  10230  fin23lem28  10253  fin23lem30  10255  compsscnvlem  10283  isf34lem2  10286  compssiso  10287  isf34lem4  10290  fin1a2lem7  10319  axcclem  10370  zornn0g  10418  ttukey2g  10429  pinn  10791  niex  10794  ltsopi  10801  dmaddpi  10803  dmmulpi  10804  lerelxr  11197  mulnzcnf  11784  dflt2  13068  expcl2lem  13998  expclzlem  14008  hashun2  14308  fsumss  15650  fsumless  15721  cvgcmpce  15743  fprodss  15873  rpnnen2lem9  16149  isstruct2  17078  structcnvcnv  17082  strleun  17086  strle1  17087  fsets  17098  mreexexlem2d  17569  gsumpropd2lem  18571  symgfixf1  19334  f1omvdmvd  19340  mvdco  19342  f1omvdconj  19343  pmtrfb  19362  pmtrfconj  19363  symggen  19367  symggen2  19368  psgnunilem1  19390  frgpnabllem2  19771  dprdss  19928  dprd2da  19941  dmdprdsplit2lem  19944  dpjidcl  19957  ablfac1b  19969  ablfac1eu  19972  isdomn3  20618  isdrng2  20646  drngmclOLD  20654  drngid2  20655  isdrngd  20668  isdrngdOLD  20670  cntzsdrg  20705  subdrgint  20706  cnmgpid  21354  cnmsubglem  21355  xrs1mnd  21365  xrs10  21366  xrs1cmn  21367  xrge0subm  21368  xrge0cmn  21369  expghm  21400  dsmmfi  21663  islinds2  21738  lindsind2  21744  lindfrn  21746  islindf4  21763  psdmul  22069  mdetdiaglem  22501  mdetrsca2  22507  mdetrlin2  22510  mdetralt  22511  mdetunilem5  22519  mdetunilem9  22523  maducoeval2  22543  smadiadetglem1  22574  isopn2  22935  ntrval2  22954  ntrdif  22955  clsdif  22956  ntrss  22958  cmclsopn  22965  discld  22992  mretopd  22995  lpsscls  23044  restntr  23085  cmpcld  23305  2ndcsep  23362  1stccnp  23365  llycmpkgen2  23453  1stckgen  23457  txkgen  23555  qtopcld  23616  qtopcmap  23622  kqdisj  23635  isufil2  23811  ufileu  23822  filufint  23823  fixufil  23825  cfinufil  23831  ufilen  23833  fin1aufil  23835  supnfcls  23923  flimfnfcls  23931  alexsublem  23947  alexsubALTlem3  23952  cldsubg  24014  imasdsf1olem  24277  recld2  24719  sszcld  24722  xrge0gsumle  24738  divcnOLD  24773  divcn  24775  cdivcncf  24830  bcth3  25247  ismbl2  25444  cmmbl  25451  nulmbl  25452  nulmbl2  25453  unmbl  25454  voliunlem1  25467  voliunlem2  25468  ioombl1lem4  25478  ioombl1  25479  uniioombllem3  25502  mbfss  25563  itg1cl  25602  itg1ge0  25603  i1f0  25604  i1f1  25607  i1fmul  25613  itg1addlem4  25616  itg1mulc  25621  itg10a  25627  itg1ge0a  25628  itg1climres  25631  itg2cnlem1  25678  itgioo  25733  itgsplitioo  25755  limcdif  25793  ellimc2  25794  ellimc3  25796  limcflflem  25797  limcflf  25798  limcmo  25799  limcresi  25802  dvreslem  25826  dvres2lem  25827  dvidlem  25832  dvcnp2  25837  dvcnp2OLD  25838  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvrec  25875  dvcnvlem  25896  lhop1lem  25934  lhop  25937  tdeglem4  25981  deg1n0ima  26010  aacjcl  26251  taylthlem2  26298  taylthlem2OLD  26299  abelth  26367  logcnlem5  26571  dvlog2  26578  efopnlem2  26582  dvcncxp1  26668  dvcnsqrt  26669  cxpcn2  26672  sqrtcn  26676  efrlim  26895  efrlimOLD  26896  jensen  26915  amgm  26917  lgamgulmlem2  26956  lgamucov  26964  wilthlem2  26995  dchrelbas2  27164  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  nnssn0s  28237  tgisline  28590  upgrss  29051  frgrwopreg2  30281  difxp1ss  32484  difxp2ss  32485  xrge00  32981  symgcom2  33039  pmtrcnel  33044  pmtrcnel2  33045  pmtrcnelor  33046  cycpmrn  33098  tocyccntz  33099  submatres  33775  madjusmdetlem2  33797  madjusmdetlem3  33798  qtophaus  33805  fsumcvg4  33919  gsumesum  34028  pwsiga  34099  sigainb  34105  carsggect  34288  omsmeas  34293  sitgclg  34312  ballotlemfelz  34461  ballotlemfp1  34462  ballotth  34508  cxpcncf1  34565  logdivsqrle  34620  hgt750lemb  34626  kur14lem6  35186  kur14lem7  35187  cvmscld  35248  satfvsucsuc  35340  satfrnmapom  35345  mclsppslem  35558  fundmpss  35742  relsset  35864  limitssson  35887  fnsingle  35895  funimage  35904  cldbnd  36302  clsun  36304  topdifinffinlem  37323  inunissunidif  37351  pibt2  37393  matunitlindflem1  37598  poimirlem8  37610  poimirlem26  37628  poimirlem30  37632  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  voliunnfl  37646  cnambfre  37650  dvtan  37652  dvasin  37686  dvacos  37687  areacirclem4  37693  fdc  37727  divrngcl  37939  isdrngo2  37940  isdrngo3  37941  islsati  38975  hdmap14lem2a  41849  redvmptabs  42336  prjspreln0  42585  prjspvs  42586  prjspeclsp  42588  0prjspnrel  42603  istopclsd  42676  diophin  42748  dnnumch1  43020  deg1mhm  43176  gneispace  44110  inaex  44273  sumnnodd  45615  cncficcgt0  45873  cncfiooicclem1  45878  cxpcncf2  45884  dirkercncflem2  46089  fourierdlem62  46153  fourierdlem66  46157  fourierdlem68  46159  fourierdlem95  46186  etransclem24  46243  etransclem44  46263  gsumge0cl  46356  sge0fodjrnlem  46401  carageniuncllem1  46506  smfresal  46773  dfnbgrss  47840  dfnbgrss2  47847  lindslinindimp2lem2  48448  iscnrm3rlem2  48929  amgmlemALT  49792