Theorem difss 3993

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

Syntax hints:   ∖ cdif 3821   ⊆ wss 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-dif 3827  df-in 3831  df-ss 3838

This theorem is referenced by:  difssd  3994  difss2  3995  ssdifss  3997  0dif  4236  disj4  4286  difsnpss  4611  unidif  4742  iunxdif2  4840  difexg  5084  reldif  5535  cnvdif  5840  difxp  5859  wfi  6017  tz7.7  6053  fresaun  6376  fresaunres2  6377  resdif  6462  fndmdif  6636  tfi  7383  peano5  7419  wfrlem16  7773  oelim2  8021  swoer  8118  swoord1  8119  swoord2  8120  ralxpmap  8257  boxcutc  8301  undom  8400  domunsncan  8412  sbthlem2  8423  sbthlem4  8425  sbthlem5  8426  limenpsi  8487  phplem2  8492  php3  8498  diffi  8544  frfi  8557  fofinf1o  8593  ixpfi2  8616  elfiun  8688  marypha1lem  8691  wemapso  8809  infdifsn  8913  cantnflem2  8946  dfac8alem  9248  acnnum  9271  inffien  9282  kmlem5  9373  infdif  9428  infdif2  9429  ackbij1lem18  9456  fictb  9464  fin23lem7  9535  fin23lem11  9536  fin23lem28  9559  fin23lem30  9561  compsscnvlem  9589  isf34lem2  9592  compssiso  9593  isf34lem4  9596  fin1a2lem7  9625  axcclem  9676  zornn0g  9724  ttukey2g  9735  pinn  10097  niex  10100  ltsopi  10107  dmaddpi  10109  dmmulpi  10110  lerelxr  10503  mulnzcnopr  11086  dflt2  12357  expcl2lem  13255  expclzlem  13267  hashun2  13556  fsumss  14941  fsumless  15010  cvgcmpce  15032  fprodss  15161  rpnnen2lem9  15434  isstruct2  16348  structcnvcnv  16352  fsets  16371  strleun  16446  strle1  16447  mreexexlem2d  16787  gsumpropd2lem  17754  symgfixf1  18339  f1omvdmvd  18345  mvdco  18347  f1omvdconj  18348  pmtrfb  18367  pmtrfconj  18368  symggen  18372  symggen2  18373  psgnunilem1  18395  frgpnabllem2  18763  dprdss  18914  dprd2da  18927  dmdprdsplit2lem  18930  dpjidcl  18943  ablfac1b  18955  ablfac1eu  18958  isdrng2  19248  drngmcl  19251  drngid2  19254  isdrngd  19263  cntzsdrg  19316  subdrgint  19317  xrs1mnd  20301  xrs10  20302  xrs1cmn  20303  xrge0subm  20304  xrge0cmn  20305  cnmgpid  20325  cnmsubglem  20326  expghm  20361  dsmmfi  20600  islinds2  20675  lindsind2  20681  lindfrn  20683  islindf4  20700  mdetdiaglem  20927  mdetrsca2  20933  mdetrlin2  20936  mdetralt  20937  mdetunilem5  20945  mdetunilem9  20949  maducoeval2  20969  smadiadetglem1  21000  isopn2  21360  ntrval2  21379  ntrdif  21380  clsdif  21381  ntrss  21383  cmclsopn  21390  discld  21417  mretopd  21420  lpsscls  21469  restntr  21510  cmpcld  21730  2ndcsep  21787  1stccnp  21790  llycmpkgen2  21878  1stckgen  21882  txkgen  21980  qtopcld  22041  qtopcmap  22047  kqdisj  22060  isufil2  22236  ufileu  22247  filufint  22248  fixufil  22250  cfinufil  22256  ufilen  22258  fin1aufil  22260  supnfcls  22348  flimfnfcls  22356  alexsublem  22372  alexsubALTlem3  22377  cldsubg  22438  imasdsf1olem  22702  recld2  23141  sszcld  23144  xrge0gsumle  23160  divcn  23195  cdivcncf  23244  bcth3  23653  ismbl2  23847  cmmbl  23854  nulmbl  23855  nulmbl2  23856  unmbl  23857  voliunlem1  23870  voliunlem2  23871  ioombl1lem4  23881  ioombl1  23882  uniioombllem3  23905  mbfss  23966  itg1cl  24005  itg1ge0  24006  i1f0  24007  i1f1  24010  i1fmul  24016  itg1addlem4  24019  itg1mulc  24024  itg10a  24030  itg1ge0a  24031  itg1climres  24034  itg2cnlem1  24081  itgioo  24135  itgsplitioo  24157  limcdif  24193  ellimc2  24194  ellimc3  24196  limcflflem  24197  limcflf  24198  limcmo  24199  limcresi  24202  dvreslem  24226  dvres2lem  24227  dvidlem  24232  dvcnp2  24236  dvaddbr  24254  dvmulbr  24255  dvcobr  24262  dvrec  24271  dvcnvlem  24292  lhop1lem  24329  lhop  24332  tdeglem4  24373  deg1n0ima  24402  aacjcl  24635  taylthlem2  24681  abelth  24748  logcnlem5  24946  dvlog2  24953  efopnlem2  24957  dvcncxp1  25041  dvcnsqrt  25042  cxpcn2  25044  sqrtcn  25048  efrlim  25265  jensen  25284  amgm  25286  lgamgulmlem2  25325  lgamucov  25333  wilthlem2  25364  dchrelbas2  25531  rpvmasum2  25806  dchrisum0re  25807  dchrisum0lem3  25813  dchrisum0  25814  tgisline  26131  upgrss  26592  frgrwopreg2  27869  difxp1ss  30073  difxp2ss  30074  xrge00  30432  submatres  30746  madjusmdetlem2  30768  madjusmdetlem3  30769  qtophaus  30777  fsumcvg4  30870  gsumesum  30995  pwsiga  31067  sigainb  31073  carsggect  31254  omsmeas  31259  sitgclg  31278  ballotlemfelz  31427  ballotlemfp1  31428  ballotth  31474  cxpcncf1  31547  logdivsqrle  31602  hgt750lemb  31608  kur14lem6  32076  kur14lem7  32077  cvmscld  32138  mclsppslem  32383  fundmpss  32562  frpoind  32634  frind  32639  frr1  32698  relsset  32903  limitssson  32926  fnsingle  32934  funimage  32943  cldbnd  33228  clsun  33230  topdifinffinlem  34103  inunissunidif  34131  pibt2  34172  matunitlindflem1  34362  poimirlem8  34374  poimirlem26  34392  poimirlem30  34396  mblfinlem3  34405  mblfinlem4  34406  ismblfin  34407  voliunnfl  34410  cnambfre  34414  dvtan  34416  dvasin  34452  dvacos  34453  areacirclem4  34459  fdc  34495  divrngcl  34710  isdrngo2  34711  isdrngo3  34712  islsati  35608  hdmap14lem2a  38481  prjspreln0  38700  prjspvs  38701  prjspeclsp  38703  0prjspnrel  38710  istopclsd  38726  diophin  38799  dnnumch1  39074  isdomn3  39234  deg1mhm  39237  gneispace  39881  inaex  40042  sumnnodd  41372  cncficcgt0  41631  cncfiooicclem1  41636  cxpcncf2  41643  dirkercncflem2  41850  fourierdlem62  41914  fourierdlem66  41918  fourierdlem68  41920  fourierdlem95  41947  etransclem24  42004  etransclem44  42024  gsumge0cl  42114  sge0fodjrnlem  42159  carageniuncllem1  42264  smfresal  42524  lindslinindimp2lem2  43911  amgmlemALT  44301