Theorem difss 4083

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

This proof depends on syntax axioms:   ∖ cdif 3896   ⊆ wss 3899

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916

This theorem is used by:  difssd  4084  difss2  4085  ssdifss  4087  0dif  4356  disj4  4412  difsnpss  4770  unidif  4903  iunxdif2  5012  difexg  5294  difelpw  5318  reldif  5796  cnvdif  6134  difxp  6156  frpoind  6340  tz7.7  6383  fresaun  6746  fresaunres2  6747  resdif  6839  fndmdif  7034  tfi  7849  peano5  7890  oelim2  8583  swoer  8728  swoord1  8729  swoord2  8730  ralxpmap  8903  boxcutc  8948  undom  9063  domunsncan  9075  sbthlem2  9086  sbthlem4  9088  sbthlem5  9089  limenpsi  9150  diffi  9169  php3  9203  frfi  9255  fofinf1o  9299  ixpfi2  9317  elfiun  9400  marypha1lem  9403  wemapso  9523  infdifsn  9636  cantnflem2  9669  frind  9732  frr1  9741  dfac8alem  10032  acnnum  10055  inffien  10066  kmlem5  10157  infdif  10210  infdif2  10211  ackbij1lem18  10238  fictb  10246  fin23lem7  10318  fin23lem11  10319  fin23lem28  10342  fin23lem30  10344  compsscnvlem  10372  isf34lem2  10375  compssiso  10376  isf34lem4  10379  fin1a2lem7  10408  axcclem  10459  zornn0g  10507  ttukey2g  10518  pinn  10887  niex  10890  ltsopi  10897  dmaddpi  10899  dmmulpi  10900  lerelxr  11296  mulnzcnf  11884  dflt2  13199  expcl2lem  14137  expclzlem  14147  hashun2  14447  fsumss  15811  fsumless  15883  cvgcmpce  15905  fprodss  16035  rpnnen2lem9  16310  isstruct2  17241  structcnvcnv  17245  strleun  17249  strle1  17250  fsets  17261  mreexexlem2d  17733  gsumpropd2lem  18781  symgfixf1  19564  f1omvdmvd  19570  mvdco  19572  f1omvdconj  19573  pmtrfb  19592  pmtrfconj  19593  symggen  19597  symggen2  19598  psgnunilem1  19620  frgpnabllem2  20001  dprdss  20158  dprd2da  20171  dmdprdsplit2lem  20174  dpjidcl  20187  ablfac1b  20199  ablfac1eu  20202  isdomn3  20876  isdrng2  20906  isdrng3lem0  20913  isdrng3lem2  20915  isdrng5  20917  drngid2  20919  isdrngd  20931  isdrngdOLD  20933  cntzsdrg  20968  subdrgint  20969  prmidlsubm  21550  cnmgpid  21642  cnmsubglem  21643  xrs1mnd  21653  xrs10  21654  xrs1cmn  21655  xrge0subm  21656  xrge0cmn  21657  expghm  21688  dsmmfi  21951  islinds2  22026  lindsind2  22032  lindfrn  22034  islindf4  22051  psdmul  22394  mdetdiaglem  22820  mdetrsca2  22826  mdetrlin2  22829  mdetralt  22830  mdetunilem5  22838  mdetunilem9  22842  maducoeval2  22862  smadiadetglem1  22893  matunitlindflem1  22901  isopn2  23257  ntrval2  23276  ntrdif  23277  clsdif  23278  ntrss  23280  cmclsopn  23287  discld  23314  mretopd  23317  lpsscls  23366  restntr  23407  cmpcld  23627  2ndcsep  23685  1stccnp  23688  llycmpkgen2  23776  1stckgen  23780  txkgen  23878  qtopcld  23939  qtopcmap  23945  kqdisj  23958  isufil2  24134  ufileu  24145  filufint  24146  fixufil  24148  cfinufil  24154  ufilen  24156  fin1aufil  24158  supnfcls  24246  flimfnfcls  24254  alexsublem  24270  alexsubALTlem3  24275  cldsubg  24337  imasdsf1olem  24599  recld2  25041  sszcld  25044  xrge0gsumle  25060  divcn  25096  cdivcncf  25149  bcth3  25559  ismbl2  25755  cmmbl  25762  nulmbl  25763  nulmbl2  25764  unmbl  25765  voliunlem1  25778  voliunlem2  25779  ioombl1lem4  25789  ioombl1  25790  uniioombllem3  25813  mbfss  25874  itg1cl  25913  itg1ge0  25914  i1f0  25915  i1f1  25918  i1fmul  25924  itg1addlem4  25927  itg1mulc  25932  itg10a  25938  itg1ge0a  25939  itg1climres  25942  itg2cnlem1  25989  itgioo  26043  itgsplitioo  26065  limcdif  26103  ellimc2  26104  ellimc3  26106  limcflflem  26107  limcflf  26108  limcmo  26109  limcresi  26112  dvreslem  26136  dvres2lem  26137  dvidlem  26142  dvcnp2  26147  dvaddbr  26165  dvmulbr  26166  dvcobr  26173  dvrec  26182  dvcnvlem  26203  lhop1lem  26240  lhop  26243  tdeglem4  26285  deg1n0ima  26314  aacjcl  26563  taylthlem2  26610  abelth  26677  logcnlem5  26883  dvlog2  26890  efopnlem2  26894  dvcncxp1  26980  dvcnsqrt  26981  cxpcn2  26983  sqrtcn  26987  efrlim  27206  jensen  27225  amgm  27227  lgamgulmlem2  27266  lgamucov  27274  wilthlem2  27305  dchrelbas2  27473  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem3  27755  dchrisum0  27756  nnssn0s  28586  tgisline  28974  upgrss  29545  frgrwopreg2  30799  difxp1ss  32997  difxp2ss  32998  xrge00  33454  symgcom2  33524  pmtrcnel  33529  pmtrcnel2  33530  pmtrcnelor  33531  cycpmrn  33583  tocyccntz  33584  evlextv  34052  vietalem  34089  submatres  34316  madjusmdetlem2  34338  madjusmdetlem3  34339  qtophaus  34346  fsumcvg4  34460  gsumesum  34569  pwsiga  34640  sigainb  34647  carsggect  34829  omsmeas  34834  sitgclg  34853  ballotlemfelz  35002  ballotlemfp1  35003  ballotth  35049  cxpcncf1  35103  logdivsqrle  35158  hgt750lemb  35164  fineqvnttrclse  35650  kur14lem6  35790  kur14lem7  35791  cvmscld  35852  satfvsucsuc  35944  satfrnmapom  35949  mclsppslem  36162  fundmpss  36346  relsset  36465  limitssson  36488  fnsingle  36496  funimage  36505  cldbnd  36945  clsun  36947  topdifinffinlem  38101  inunissunidif  38129  pibt2  38171  poimirlem8  38377  poimirlem26  38395  poimirlem30  38399  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  voliunnfl  38413  cnambfre  38417  dvtan  38419  dvasin  38453  dvacos  38454  areacirclem4  38460  fdc  38495  divrngcl  38707  isdrngo2  38708  isdrngo3  38709  islsati  39867  hdmap14lem2a  42740  redvmptabs  43235  prjspreln0  43455  prjspvs  43456  prjspeclsp  43458  0prjspnrel  43473  istopclsd  43545  diophin  43617  dnnumch1  43885  deg1mhm  44041  gneispace  44974  inaex  45121  sumnnodd  46460  cncficcgt0  46716  cncfiooicclem1  46721  cxpcncf2  46727  dirkercncflem2  46932  fourierdlem62  46996  fourierdlem66  47000  fourierdlem68  47002  fourierdlem95  47029  etransclem24  47086  etransclem44  47106  gsumge0cl  47199  sge0fodjrnlem  47244  carageniuncllem1  47349  smfresal  47616  dfnbgrss  48768  dfnbgrss2  48775  lindslinindimp2lem2  49389  iscnrm3rlem2  49867  amgmlemALT  50821