Theorem difss 4145

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

Syntax hints:   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  difssd  4146  difss2  4147  ssdifss  4149  0dif  4410  disj4  4464  difsnpss  4811  unidif  4946  iunxdif2  5057  difexg  5334  difelpw  5359  reldif  5827  cnvdif  6165  difxp  6185  frpoind  6364  wfiOLD  6373  tz7.7  6411  fresaun  6779  fresaunres2  6780  resdif  6869  fndmdif  7061  tfi  7873  peano5  7915  wfrlem16OLD  8362  oelim2  8631  swoer  8774  swoord1  8775  swoord2  8776  ralxpmap  8934  boxcutc  8979  undom  9097  undomOLD  9098  domunsncan  9110  sbthlem2  9122  sbthlem4  9124  sbthlem5  9125  limenpsi  9190  diffi  9213  php3  9246  phplem2OLD  9252  php3OLD  9258  frfi  9318  fofinf1o  9369  ixpfi2  9387  elfiun  9467  marypha1lem  9470  wemapso  9588  infdifsn  9694  cantnflem2  9727  frind  9787  frr1  9796  dfac8alem  10066  acnnum  10089  inffien  10100  kmlem5  10192  infdif  10245  infdif2  10246  ackbij1lem18  10273  fictb  10281  fin23lem7  10353  fin23lem11  10354  fin23lem28  10377  fin23lem30  10379  compsscnvlem  10407  isf34lem2  10410  compssiso  10411  isf34lem4  10414  fin1a2lem7  10443  axcclem  10494  zornn0g  10542  ttukey2g  10553  pinn  10915  niex  10918  ltsopi  10925  dmaddpi  10927  dmmulpi  10928  lerelxr  11321  mulnzcnf  11906  dflt2  13186  expcl2lem  14110  expclzlem  14120  hashun2  14418  fsumss  15757  fsumless  15828  cvgcmpce  15850  fprodss  15980  rpnnen2lem9  16254  isstruct2  17182  structcnvcnv  17186  strleun  17190  strle1  17191  fsets  17202  mreexexlem2d  17689  gsumpropd2lem  18704  symgfixf1  19469  f1omvdmvd  19475  mvdco  19477  f1omvdconj  19478  pmtrfb  19497  pmtrfconj  19498  symggen  19502  symggen2  19503  psgnunilem1  19525  frgpnabllem2  19906  dprdss  20063  dprd2da  20076  dmdprdsplit2lem  20079  dpjidcl  20092  ablfac1b  20104  ablfac1eu  20107  isdomn3  20731  isdrng2  20759  drngmclOLD  20767  drngid2  20768  isdrngd  20781  isdrngdOLD  20783  cntzsdrg  20819  subdrgint  20820  xrs1mnd  21439  xrs10  21440  xrs1cmn  21441  xrge0subm  21442  xrge0cmn  21443  cnmgpid  21464  cnmsubglem  21465  expghm  21503  dsmmfi  21775  islinds2  21850  lindsind2  21856  lindfrn  21858  islindf4  21875  psdmul  22187  mdetdiaglem  22619  mdetrsca2  22625  mdetrlin2  22628  mdetralt  22629  mdetunilem5  22637  mdetunilem9  22641  maducoeval2  22661  smadiadetglem1  22692  isopn2  23055  ntrval2  23074  ntrdif  23075  clsdif  23076  ntrss  23078  cmclsopn  23085  discld  23112  mretopd  23115  lpsscls  23164  restntr  23205  cmpcld  23425  2ndcsep  23482  1stccnp  23485  llycmpkgen2  23573  1stckgen  23577  txkgen  23675  qtopcld  23736  qtopcmap  23742  kqdisj  23755  isufil2  23931  ufileu  23942  filufint  23943  fixufil  23945  cfinufil  23951  ufilen  23953  fin1aufil  23955  supnfcls  24043  flimfnfcls  24051  alexsublem  24067  alexsubALTlem3  24072  cldsubg  24134  imasdsf1olem  24398  recld2  24849  sszcld  24852  xrge0gsumle  24868  divcnOLD  24903  divcn  24905  cdivcncf  24960  bcth3  25378  ismbl2  25575  cmmbl  25582  nulmbl  25583  nulmbl2  25584  unmbl  25585  voliunlem1  25598  voliunlem2  25599  ioombl1lem4  25609  ioombl1  25610  uniioombllem3  25633  mbfss  25694  itg1cl  25733  itg1ge0  25734  i1f0  25735  i1f1  25738  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  itg1mulc  25753  itg10a  25759  itg1ge0a  25760  itg1climres  25763  itg2cnlem1  25810  itgioo  25865  itgsplitioo  25887  limcdif  25925  ellimc2  25926  ellimc3  25928  limcflflem  25929  limcflf  25930  limcmo  25931  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvrec  26007  dvcnvlem  26028  lhop1lem  26066  lhop  26069  tdeglem4  26113  deg1n0ima  26142  aacjcl  26383  taylthlem2  26430  taylthlem2OLD  26431  abelth  26499  logcnlem5  26702  dvlog2  26709  efopnlem2  26713  dvcncxp1  26799  dvcnsqrt  26800  cxpcn2  26803  sqrtcn  26807  efrlim  27026  efrlimOLD  27027  jensen  27046  amgm  27048  lgamgulmlem2  27087  lgamucov  27095  wilthlem2  27126  dchrelbas2  27295  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem3  27577  dchrisum0  27578  nnssn0s  28340  tgisline  28649  upgrss  29119  frgrwopreg2  30347  difxp1ss  32549  difxp2ss  32550  xrge00  32999  symgcom2  33086  pmtrcnel  33091  pmtrcnel2  33092  pmtrcnelor  33093  cycpmrn  33145  tocyccntz  33146  submatres  33766  madjusmdetlem2  33788  madjusmdetlem3  33789  qtophaus  33796  fsumcvg4  33910  gsumesum  34039  pwsiga  34110  sigainb  34116  carsggect  34299  omsmeas  34304  sitgclg  34323  ballotlemfelz  34471  ballotlemfp1  34472  ballotth  34518  cxpcncf1  34588  logdivsqrle  34643  hgt750lemb  34649  kur14lem6  35195  kur14lem7  35196  cvmscld  35257  satfvsucsuc  35349  satfrnmapom  35354  mclsppslem  35567  fundmpss  35747  relsset  35869  limitssson  35892  fnsingle  35900  funimage  35909  cldbnd  36308  clsun  36310  topdifinffinlem  37329  inunissunidif  37357  pibt2  37399  matunitlindflem1  37602  poimirlem8  37614  poimirlem26  37632  poimirlem30  37636  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  voliunnfl  37650  cnambfre  37654  dvtan  37656  dvasin  37690  dvacos  37691  areacirclem4  37697  fdc  37731  divrngcl  37943  isdrngo2  37944  isdrngo3  37945  islsati  38975  hdmap14lem2a  41849  redvmptabs  42368  prjspreln0  42595  prjspvs  42596  prjspeclsp  42598  0prjspnrel  42613  istopclsd  42687  diophin  42759  dnnumch1  43032  deg1mhm  43188  gneispace  44123  inaex  44292  sumnnodd  45585  cncficcgt0  45843  cncfiooicclem1  45848  cxpcncf2  45854  dirkercncflem2  46059  fourierdlem62  46123  fourierdlem66  46127  fourierdlem68  46129  fourierdlem95  46156  etransclem24  46213  etransclem44  46233  gsumge0cl  46326  sge0fodjrnlem  46371  carageniuncllem1  46476  smfresal  46743  dfnbgrss  47775  dfnbgrss2  47782  lindslinindimp2lem2  48304  iscnrm3rlem2  48737  amgmlemALT  49033