Theorem difss 4090

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

This proof depends on syntax axioms:   ∖ cdif 3903   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  difssd  4091  difss2  4092  ssdifss  4094  0dif  4363  disj4  4419  difsnpss  4777  unidif  4910  iunxdif2  5020  difexg  5302  difelpw  5326  reldif  5804  cnvdif  6142  difxp  6163  frpoind  6347  tz7.7  6390  fresaun  6753  fresaunres2  6754  resdif  6846  fndmdif  7041  tfi  7851  peano5  7892  oelim2  8583  swoer  8728  swoord1  8729  swoord2  8730  ralxpmap  8896  boxcutc  8941  undom  9056  domunsncan  9068  sbthlem2  9079  sbthlem4  9081  sbthlem5  9082  limenpsi  9143  diffi  9162  php3  9196  frfi  9248  fofinf1o  9292  ixpfi2  9310  elfiun  9393  marypha1lem  9396  wemapso  9516  infdifsn  9629  cantnflem2  9662  frind  9725  frr1  9734  dfac8alem  10025  acnnum  10048  inffien  10059  kmlem5  10150  infdif  10203  infdif2  10204  ackbij1lem18  10231  fictb  10239  fin23lem7  10311  fin23lem11  10312  fin23lem28  10335  fin23lem30  10337  compsscnvlem  10365  isf34lem2  10368  compssiso  10369  isf34lem4  10372  fin1a2lem7  10401  axcclem  10452  zornn0g  10500  ttukey2g  10511  pinn  10874  niex  10877  ltsopi  10884  dmaddpi  10886  dmmulpi  10887  lerelxr  11283  mulnzcnf  11871  dflt2  13184  expcl2lem  14122  expclzlem  14132  hashun2  14432  fsumss  15794  fsumless  15866  cvgcmpce  15888  fprodss  16020  rpnnen2lem9  16295  isstruct2  17226  structcnvcnv  17230  strleun  17234  strle1  17235  fsets  17246  mreexexlem2d  17718  gsumpropd2lem  18758  symgfixf1  19530  f1omvdmvd  19536  mvdco  19538  f1omvdconj  19539  pmtrfb  19558  pmtrfconj  19559  symggen  19563  symggen2  19564  psgnunilem1  19586  frgpnabllem2  19967  dprdss  20124  dprd2da  20137  dmdprdsplit2lem  20140  dpjidcl  20153  ablfac1b  20165  ablfac1eu  20168  isdomn3  20842  isdrng2  20872  isdrng3lem0  20879  isdrng3lem2  20881  isdrng5  20883  drngid2  20885  isdrngd  20897  isdrngdOLD  20899  cntzsdrg  20934  subdrgint  20935  prmidlsubm  21516  cnmgpid  21608  cnmsubglem  21609  xrs1mnd  21619  xrs10  21620  xrs1cmn  21621  xrge0subm  21622  xrge0cmn  21623  expghm  21654  dsmmfi  21917  islinds2  21992  lindsind2  21998  lindfrn  22000  islindf4  22017  psdmul  22358  mdetdiaglem  22784  mdetrsca2  22790  mdetrlin2  22793  mdetralt  22794  mdetunilem5  22802  mdetunilem9  22806  maducoeval2  22826  smadiadetglem1  22857  isopn2  23218  ntrval2  23237  ntrdif  23238  clsdif  23239  ntrss  23241  cmclsopn  23248  discld  23275  mretopd  23278  lpsscls  23327  restntr  23368  cmpcld  23588  2ndcsep  23645  1stccnp  23648  llycmpkgen2  23736  1stckgen  23740  txkgen  23838  qtopcld  23899  qtopcmap  23905  kqdisj  23918  isufil2  24094  ufileu  24105  filufint  24106  fixufil  24108  cfinufil  24114  ufilen  24116  fin1aufil  24118  supnfcls  24206  flimfnfcls  24214  alexsublem  24230  alexsubALTlem3  24235  cldsubg  24297  imasdsf1olem  24559  recld2  25001  sszcld  25004  xrge0gsumle  25020  divcn  25056  cdivcncf  25109  bcth3  25519  ismbl2  25715  cmmbl  25722  nulmbl  25723  nulmbl2  25724  unmbl  25725  voliunlem1  25738  voliunlem2  25739  ioombl1lem4  25749  ioombl1  25750  uniioombllem3  25773  mbfss  25834  itg1cl  25873  itg1ge0  25874  i1f0  25875  i1f1  25878  i1fmul  25884  itg1addlem4  25887  itg1mulc  25892  itg10a  25898  itg1ge0a  25899  itg1climres  25902  itg2cnlem1  25949  itgioo  26004  itgsplitioo  26026  limcdif  26064  ellimc2  26065  ellimc3  26067  limcflflem  26068  limcflf  26069  limcmo  26070  limcresi  26073  dvreslem  26097  dvres2lem  26098  dvidlem  26103  dvcnp2  26108  dvaddbr  26126  dvmulbr  26127  dvcobr  26134  dvrec  26143  dvcnvlem  26164  lhop1lem  26201  lhop  26204  tdeglem4  26246  deg1n0ima  26275  aacjcl  26519  taylthlem2  26566  abelth  26633  logcnlem5  26840  dvlog2  26847  efopnlem2  26851  dvcncxp1  26937  dvcnsqrt  26938  cxpcn2  26940  sqrtcn  26944  efrlim  27163  jensen  27182  amgm  27184  lgamgulmlem2  27223  lgamucov  27231  wilthlem2  27262  dchrelbas2  27430  rpvmasum2  27705  dchrisum0re  27706  dchrisum0lem3  27712  dchrisum0  27713  nnssn0s  28543  tgisline  28929  upgrss  29467  frgrwopreg2  30699  difxp1ss  32897  difxp2ss  32898  xrge00  33357  symgcom2  33427  pmtrcnel  33432  pmtrcnel2  33433  pmtrcnelor  33434  cycpmrn  33486  tocyccntz  33487  evlextv  33955  vietalem  33992  submatres  34219  madjusmdetlem2  34241  madjusmdetlem3  34242  qtophaus  34249  fsumcvg4  34363  gsumesum  34472  pwsiga  34543  sigainb  34550  carsggect  34732  omsmeas  34737  sitgclg  34756  ballotlemfelz  34905  ballotlemfp1  34906  ballotth  34952  cxpcncf1  35006  logdivsqrle  35061  hgt750lemb  35067  fineqvnttrclse  35553  kur14lem6  35716  kur14lem7  35717  cvmscld  35778  satfvsucsuc  35870  satfrnmapom  35875  mclsppslem  36088  fundmpss  36272  relsset  36391  limitssson  36414  fnsingle  36422  funimage  36431  cldbnd  36870  clsun  36872  topdifinffinlem  38026  inunissunidif  38054  pibt2  38096  matunitlindflem1  38300  poimirlem8  38312  poimirlem26  38330  poimirlem30  38334  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  voliunnfl  38348  cnambfre  38352  dvtan  38354  dvasin  38388  dvacos  38389  areacirclem4  38395  fdc  38429  divrngcl  38641  isdrngo2  38642  isdrngo3  38643  islsati  39801  hdmap14lem2a  42674  redvmptabs  43154  prjspreln0  43374  prjspvs  43375  prjspeclsp  43377  0prjspnrel  43392  istopclsd  43464  diophin  43536  dnnumch1  43804  deg1mhm  43960  gneispace  44893  inaex  45040  sumnnodd  46379  cncficcgt0  46635  cncfiooicclem1  46640  cxpcncf2  46646  dirkercncflem2  46851  fourierdlem62  46915  fourierdlem66  46919  fourierdlem68  46921  fourierdlem95  46948  etransclem24  47005  etransclem44  47025  gsumge0cl  47118  sge0fodjrnlem  47163  carageniuncllem1  47268  smfresal  47535  dfnbgrss  48650  dfnbgrss2  48657  lindslinindimp2lem2  49272  iscnrm3rlem2  49752  amgmlemALT  50684