Theorem difss 4076

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

Syntax hints:   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  difssd  4077  difss2  4078  ssdifss  4080  0dif  4345  disj4  4399  difsnpss  4752  unidif  4885  iunxdif2  4996  difexg  5270  difelpw  5295  reldif  5771  cnvdif  6107  difxp  6128  frpoind  6306  tz7.7  6349  fresaun  6711  fresaunres2  6712  resdif  6801  fndmdif  6994  tfi  7804  peano5  7844  oelim2  8531  swoer  8675  swoord1  8676  swoord2  8677  ralxpmap  8844  boxcutc  8889  undom  9003  domunsncan  9015  sbthlem2  9026  sbthlem4  9028  sbthlem5  9029  limenpsi  9090  diffi  9109  php3  9143  frfi  9195  fofinf1o  9242  ixpfi2  9260  elfiun  9343  marypha1lem  9346  wemapso  9466  infdifsn  9578  cantnflem2  9611  frind  9674  frr1  9683  dfac8alem  9951  acnnum  9974  inffien  9985  kmlem5  10077  infdif  10130  infdif2  10131  ackbij1lem18  10158  fictb  10166  fin23lem7  10238  fin23lem11  10239  fin23lem28  10262  fin23lem30  10264  compsscnvlem  10292  isf34lem2  10295  compssiso  10296  isf34lem4  10299  fin1a2lem7  10328  axcclem  10379  zornn0g  10427  ttukey2g  10438  pinn  10801  niex  10804  ltsopi  10811  dmaddpi  10813  dmmulpi  10814  lerelxr  11208  mulnzcnf  11796  dflt2  13099  expcl2lem  14035  expclzlem  14045  hashun2  14345  fsumss  15687  fsumless  15759  cvgcmpce  15781  fprodss  15913  rpnnen2lem9  16189  isstruct2  17119  structcnvcnv  17123  strleun  17127  strle1  17128  fsets  17139  mreexexlem2d  17611  gsumpropd2lem  18647  symgfixf1  19412  f1omvdmvd  19418  mvdco  19420  f1omvdconj  19421  pmtrfb  19440  pmtrfconj  19441  symggen  19445  symggen2  19446  psgnunilem1  19468  frgpnabllem2  19849  dprdss  20006  dprd2da  20019  dmdprdsplit2lem  20022  dpjidcl  20035  ablfac1b  20047  ablfac1eu  20050  isdomn3  20692  isdrng2  20720  drngmclOLD  20728  drngid2  20729  isdrngd  20742  isdrngdOLD  20744  cntzsdrg  20779  subdrgint  20780  cnmgpid  21409  cnmsubglem  21410  xrs1mnd  21420  xrs10  21421  xrs1cmn  21422  xrge0subm  21423  xrge0cmn  21424  expghm  21455  dsmmfi  21718  islinds2  21793  lindsind2  21799  lindfrn  21801  islindf4  21818  psdmul  22132  mdetdiaglem  22563  mdetrsca2  22569  mdetrlin2  22572  mdetralt  22573  mdetunilem5  22581  mdetunilem9  22585  maducoeval2  22605  smadiadetglem1  22636  isopn2  22997  ntrval2  23016  ntrdif  23017  clsdif  23018  ntrss  23020  cmclsopn  23027  discld  23054  mretopd  23057  lpsscls  23106  restntr  23147  cmpcld  23367  2ndcsep  23424  1stccnp  23427  llycmpkgen2  23515  1stckgen  23519  txkgen  23617  qtopcld  23678  qtopcmap  23684  kqdisj  23697  isufil2  23873  ufileu  23884  filufint  23885  fixufil  23887  cfinufil  23893  ufilen  23895  fin1aufil  23897  supnfcls  23985  flimfnfcls  23993  alexsublem  24009  alexsubALTlem3  24014  cldsubg  24076  imasdsf1olem  24338  recld2  24780  sszcld  24783  xrge0gsumle  24799  divcn  24835  cdivcncf  24888  bcth3  25298  ismbl2  25494  cmmbl  25501  nulmbl  25502  nulmbl2  25503  unmbl  25504  voliunlem1  25517  voliunlem2  25518  ioombl1lem4  25528  ioombl1  25529  uniioombllem3  25552  mbfss  25613  itg1cl  25652  itg1ge0  25653  i1f0  25654  i1f1  25657  i1fmul  25663  itg1addlem4  25666  itg1mulc  25671  itg10a  25677  itg1ge0a  25678  itg1climres  25681  itg2cnlem1  25728  itgioo  25783  itgsplitioo  25805  limcdif  25843  ellimc2  25844  ellimc3  25846  limcflflem  25847  limcflf  25848  limcmo  25849  limcresi  25852  dvreslem  25876  dvres2lem  25877  dvidlem  25882  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvcobr  25913  dvrec  25922  dvcnvlem  25943  lhop1lem  25980  lhop  25983  tdeglem4  26025  deg1n0ima  26054  aacjcl  26293  taylthlem2  26339  abelth  26406  logcnlem5  26610  dvlog2  26617  efopnlem2  26621  dvcncxp1  26707  dvcnsqrt  26708  cxpcn2  26710  sqrtcn  26714  efrlim  26933  jensen  26952  amgm  26954  lgamgulmlem2  26993  lgamucov  27001  wilthlem2  27032  dchrelbas2  27200  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  nnssn0s  28313  tgisline  28695  upgrss  29157  frgrwopreg2  30389  difxp1ss  32592  difxp2ss  32593  xrge00  33074  symgcom2  33145  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  cycpmrn  33204  tocyccntz  33205  evlextv  33686  vietalem  33723  submatres  33950  madjusmdetlem2  33972  madjusmdetlem3  33973  qtophaus  33980  fsumcvg4  34094  gsumesum  34203  pwsiga  34274  sigainb  34280  carsggect  34462  omsmeas  34467  sitgclg  34486  ballotlemfelz  34635  ballotlemfp1  34636  ballotth  34682  cxpcncf1  34739  logdivsqrle  34794  hgt750lemb  34800  fineqvnttrclse  35268  kur14lem6  35393  kur14lem7  35394  cvmscld  35455  satfvsucsuc  35547  satfrnmapom  35552  mclsppslem  35765  fundmpss  35949  relsset  36068  limitssson  36091  fnsingle  36099  funimage  36108  cldbnd  36508  clsun  36510  topdifinffinlem  37663  inunissunidif  37691  pibt2  37733  matunitlindflem1  37937  poimirlem8  37949  poimirlem26  37967  poimirlem30  37971  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  voliunnfl  37985  cnambfre  37989  dvtan  37991  dvasin  38025  dvacos  38026  areacirclem4  38032  fdc  38066  divrngcl  38278  isdrngo2  38279  isdrngo3  38280  islsati  39440  hdmap14lem2a  42313  redvmptabs  42792  prjspreln0  43042  prjspvs  43043  prjspeclsp  43045  0prjspnrel  43060  istopclsd  43132  diophin  43204  dnnumch1  43472  deg1mhm  43628  gneispace  44561  inaex  44724  sumnnodd  46060  cncficcgt0  46316  cncfiooicclem1  46321  cxpcncf2  46327  dirkercncflem2  46532  fourierdlem62  46596  fourierdlem66  46600  fourierdlem68  46602  fourierdlem95  46629  etransclem24  46686  etransclem44  46706  gsumge0cl  46799  sge0fodjrnlem  46844  carageniuncllem1  46949  smfresal  47216  dfnbgrss  48328  dfnbgrss2  48335  lindslinindimp2lem2  48935  iscnrm3rlem2  49416  amgmlemALT  50278