Theorem difss 4085

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

Syntax hints:   ∖ cdif 3895   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915

This theorem is referenced by:  difssd  4086  difss2  4087  ssdifss  4089  0dif  4354  disj4  4408  difsnpss  4760  unidif  4895  iunxdif2  5006  difexg  5271  difelpw  5296  reldif  5761  cnvdif  6097  difxp  6118  frpoind  6296  tz7.7  6339  fresaun  6701  fresaunres2  6702  resdif  6791  fndmdif  6983  tfi  7791  peano5  7831  oelim2  8518  swoer  8661  swoord1  8662  swoord2  8663  ralxpmap  8828  boxcutc  8873  undom  8987  domunsncan  8999  sbthlem2  9010  sbthlem4  9012  sbthlem5  9013  limenpsi  9074  diffi  9093  php3  9127  frfi  9178  fofinf1o  9225  ixpfi2  9243  elfiun  9323  marypha1lem  9326  wemapso  9446  infdifsn  9556  cantnflem2  9589  frind  9652  frr1  9661  dfac8alem  9929  acnnum  9952  inffien  9963  kmlem5  10055  infdif  10108  infdif2  10109  ackbij1lem18  10136  fictb  10144  fin23lem7  10216  fin23lem11  10217  fin23lem28  10240  fin23lem30  10242  compsscnvlem  10270  isf34lem2  10273  compssiso  10274  isf34lem4  10277  fin1a2lem7  10306  axcclem  10357  zornn0g  10405  ttukey2g  10416  pinn  10778  niex  10781  ltsopi  10788  dmaddpi  10790  dmmulpi  10791  lerelxr  11184  mulnzcnf  11772  dflt2  13051  expcl2lem  13984  expclzlem  13994  hashun2  14294  fsumss  15636  fsumless  15707  cvgcmpce  15729  fprodss  15859  rpnnen2lem9  16135  isstruct2  17064  structcnvcnv  17068  strleun  17072  strle1  17073  fsets  17084  mreexexlem2d  17555  gsumpropd2lem  18591  symgfixf1  19353  f1omvdmvd  19359  mvdco  19361  f1omvdconj  19362  pmtrfb  19381  pmtrfconj  19382  symggen  19386  symggen2  19387  psgnunilem1  19409  frgpnabllem2  19790  dprdss  19947  dprd2da  19960  dmdprdsplit2lem  19963  dpjidcl  19976  ablfac1b  19988  ablfac1eu  19991  isdomn3  20634  isdrng2  20662  drngmclOLD  20670  drngid2  20671  isdrngd  20684  isdrngdOLD  20686  cntzsdrg  20721  subdrgint  20722  cnmgpid  21370  cnmsubglem  21371  xrs1mnd  21381  xrs10  21382  xrs1cmn  21383  xrge0subm  21384  xrge0cmn  21385  expghm  21416  dsmmfi  21679  islinds2  21754  lindsind2  21760  lindfrn  21762  islindf4  21779  psdmul  22084  mdetdiaglem  22516  mdetrsca2  22522  mdetrlin2  22525  mdetralt  22526  mdetunilem5  22534  mdetunilem9  22538  maducoeval2  22558  smadiadetglem1  22589  isopn2  22950  ntrval2  22969  ntrdif  22970  clsdif  22971  ntrss  22973  cmclsopn  22980  discld  23007  mretopd  23010  lpsscls  23059  restntr  23100  cmpcld  23320  2ndcsep  23377  1stccnp  23380  llycmpkgen2  23468  1stckgen  23472  txkgen  23570  qtopcld  23631  qtopcmap  23637  kqdisj  23650  isufil2  23826  ufileu  23837  filufint  23838  fixufil  23840  cfinufil  23846  ufilen  23848  fin1aufil  23850  supnfcls  23938  flimfnfcls  23946  alexsublem  23962  alexsubALTlem3  23967  cldsubg  24029  imasdsf1olem  24291  recld2  24733  sszcld  24736  xrge0gsumle  24752  divcnOLD  24787  divcn  24789  cdivcncf  24844  bcth3  25261  ismbl2  25458  cmmbl  25465  nulmbl  25466  nulmbl2  25467  unmbl  25468  voliunlem1  25481  voliunlem2  25482  ioombl1lem4  25492  ioombl1  25493  uniioombllem3  25516  mbfss  25577  itg1cl  25616  itg1ge0  25617  i1f0  25618  i1f1  25621  i1fmul  25627  itg1addlem4  25630  itg1mulc  25635  itg10a  25641  itg1ge0a  25642  itg1climres  25645  itg2cnlem1  25692  itgioo  25747  itgsplitioo  25769  limcdif  25807  ellimc2  25808  ellimc3  25810  limcflflem  25811  limcflf  25812  limcmo  25813  limcresi  25816  dvreslem  25840  dvres2lem  25841  dvidlem  25846  dvcnp2  25851  dvcnp2OLD  25852  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvcobr  25879  dvcobrOLD  25880  dvrec  25889  dvcnvlem  25910  lhop1lem  25948  lhop  25951  tdeglem4  25995  deg1n0ima  26024  aacjcl  26265  taylthlem2  26312  taylthlem2OLD  26313  abelth  26381  logcnlem5  26585  dvlog2  26592  efopnlem2  26596  dvcncxp1  26682  dvcnsqrt  26683  cxpcn2  26686  sqrtcn  26690  efrlim  26909  efrlimOLD  26910  jensen  26929  amgm  26931  lgamgulmlem2  26970  lgamucov  26978  wilthlem2  27009  dchrelbas2  27178  rpvmasum2  27453  dchrisum0re  27454  dchrisum0lem3  27460  dchrisum0  27461  nnssn0s  28253  tgisline  28608  upgrss  29070  frgrwopreg2  30303  difxp1ss  32506  difxp2ss  32507  xrge00  33004  symgcom2  33062  pmtrcnel  33067  pmtrcnel2  33068  pmtrcnelor  33069  cycpmrn  33121  tocyccntz  33122  submatres  33842  madjusmdetlem2  33864  madjusmdetlem3  33865  qtophaus  33872  fsumcvg4  33986  gsumesum  34095  pwsiga  34166  sigainb  34172  carsggect  34354  omsmeas  34359  sitgclg  34378  ballotlemfelz  34527  ballotlemfp1  34528  ballotth  34574  cxpcncf1  34631  logdivsqrle  34686  hgt750lemb  34692  fineqvnttrclse  35167  kur14lem6  35278  kur14lem7  35279  cvmscld  35340  satfvsucsuc  35432  satfrnmapom  35437  mclsppslem  35650  fundmpss  35834  relsset  35953  limitssson  35976  fnsingle  35984  funimage  35993  cldbnd  36393  clsun  36395  topdifinffinlem  37414  inunissunidif  37442  pibt2  37484  matunitlindflem1  37679  poimirlem8  37691  poimirlem26  37709  poimirlem30  37713  mblfinlem3  37722  mblfinlem4  37723  ismblfin  37724  voliunnfl  37727  cnambfre  37731  dvtan  37733  dvasin  37767  dvacos  37768  areacirclem4  37774  fdc  37808  divrngcl  38020  isdrngo2  38021  isdrngo3  38022  islsati  39116  hdmap14lem2a  41989  redvmptabs  42481  prjspreln0  42730  prjspvs  42731  prjspeclsp  42733  0prjspnrel  42748  istopclsd  42820  diophin  42892  dnnumch1  43164  deg1mhm  43320  gneispace  44254  inaex  44417  sumnnodd  45757  cncficcgt0  46013  cncfiooicclem1  46018  cxpcncf2  46024  dirkercncflem2  46229  fourierdlem62  46293  fourierdlem66  46297  fourierdlem68  46299  fourierdlem95  46326  etransclem24  46383  etransclem44  46403  gsumge0cl  46496  sge0fodjrnlem  46541  carageniuncllem1  46646  smfresal  46913  dfnbgrss  47979  dfnbgrss2  47986  lindslinindimp2lem2  48587  iscnrm3rlem2  49068  amgmlemALT  49931