Theorem difss 4136

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

Syntax hints:   ∖ cdif 3948   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968

This theorem is referenced by:  difssd  4137  difss2  4138  ssdifss  4140  0dif  4405  disj4  4459  difsnpss  4807  unidif  4942  iunxdif2  5053  difexg  5329  difelpw  5354  reldif  5825  cnvdif  6163  difxp  6184  frpoind  6363  wfiOLD  6372  tz7.7  6410  fresaun  6779  fresaunres2  6780  resdif  6869  fndmdif  7062  tfi  7874  peano5  7915  wfrlem16OLD  8364  oelim2  8633  swoer  8776  swoord1  8777  swoord2  8778  ralxpmap  8936  boxcutc  8981  undom  9099  undomOLD  9100  domunsncan  9112  sbthlem2  9124  sbthlem4  9126  sbthlem5  9127  limenpsi  9192  diffi  9215  php3  9249  phplem2OLD  9255  php3OLD  9261  frfi  9321  fofinf1o  9372  ixpfi2  9390  elfiun  9470  marypha1lem  9473  wemapso  9591  infdifsn  9697  cantnflem2  9730  frind  9790  frr1  9799  dfac8alem  10069  acnnum  10092  inffien  10103  kmlem5  10195  infdif  10248  infdif2  10249  ackbij1lem18  10276  fictb  10284  fin23lem7  10356  fin23lem11  10357  fin23lem28  10380  fin23lem30  10382  compsscnvlem  10410  isf34lem2  10413  compssiso  10414  isf34lem4  10417  fin1a2lem7  10446  axcclem  10497  zornn0g  10545  ttukey2g  10556  pinn  10918  niex  10921  ltsopi  10928  dmaddpi  10930  dmmulpi  10931  lerelxr  11324  mulnzcnf  11909  dflt2  13190  expcl2lem  14114  expclzlem  14124  hashun2  14422  fsumss  15761  fsumless  15832  cvgcmpce  15854  fprodss  15984  rpnnen2lem9  16258  isstruct2  17186  structcnvcnv  17190  strleun  17194  strle1  17195  fsets  17206  mreexexlem2d  17688  gsumpropd2lem  18692  symgfixf1  19455  f1omvdmvd  19461  mvdco  19463  f1omvdconj  19464  pmtrfb  19483  pmtrfconj  19484  symggen  19488  symggen2  19489  psgnunilem1  19511  frgpnabllem2  19892  dprdss  20049  dprd2da  20062  dmdprdsplit2lem  20065  dpjidcl  20078  ablfac1b  20090  ablfac1eu  20093  isdomn3  20715  isdrng2  20743  drngmclOLD  20751  drngid2  20752  isdrngd  20765  isdrngdOLD  20767  cntzsdrg  20803  subdrgint  20804  xrs1mnd  21422  xrs10  21423  xrs1cmn  21424  xrge0subm  21425  xrge0cmn  21426  cnmgpid  21447  cnmsubglem  21448  expghm  21486  dsmmfi  21758  islinds2  21833  lindsind2  21839  lindfrn  21841  islindf4  21858  psdmul  22170  mdetdiaglem  22604  mdetrsca2  22610  mdetrlin2  22613  mdetralt  22614  mdetunilem5  22622  mdetunilem9  22626  maducoeval2  22646  smadiadetglem1  22677  isopn2  23040  ntrval2  23059  ntrdif  23060  clsdif  23061  ntrss  23063  cmclsopn  23070  discld  23097  mretopd  23100  lpsscls  23149  restntr  23190  cmpcld  23410  2ndcsep  23467  1stccnp  23470  llycmpkgen2  23558  1stckgen  23562  txkgen  23660  qtopcld  23721  qtopcmap  23727  kqdisj  23740  isufil2  23916  ufileu  23927  filufint  23928  fixufil  23930  cfinufil  23936  ufilen  23938  fin1aufil  23940  supnfcls  24028  flimfnfcls  24036  alexsublem  24052  alexsubALTlem3  24057  cldsubg  24119  imasdsf1olem  24383  recld2  24836  sszcld  24839  xrge0gsumle  24855  divcnOLD  24890  divcn  24892  cdivcncf  24947  bcth3  25365  ismbl2  25562  cmmbl  25569  nulmbl  25570  nulmbl2  25571  unmbl  25572  voliunlem1  25585  voliunlem2  25586  ioombl1lem4  25596  ioombl1  25597  uniioombllem3  25620  mbfss  25681  itg1cl  25720  itg1ge0  25721  i1f0  25722  i1f1  25725  i1fmul  25731  itg1addlem4  25734  itg1mulc  25739  itg10a  25745  itg1ge0a  25746  itg1climres  25749  itg2cnlem1  25796  itgioo  25851  itgsplitioo  25873  limcdif  25911  ellimc2  25912  ellimc3  25914  limcflflem  25915  limcflf  25916  limcmo  25917  limcresi  25920  dvreslem  25944  dvres2lem  25945  dvidlem  25950  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvrec  25993  dvcnvlem  26014  lhop1lem  26052  lhop  26055  tdeglem4  26099  deg1n0ima  26128  aacjcl  26369  taylthlem2  26416  taylthlem2OLD  26417  abelth  26485  logcnlem5  26688  dvlog2  26695  efopnlem2  26699  dvcncxp1  26785  dvcnsqrt  26786  cxpcn2  26789  sqrtcn  26793  efrlim  27012  efrlimOLD  27013  jensen  27032  amgm  27034  lgamgulmlem2  27073  lgamucov  27081  wilthlem2  27112  dchrelbas2  27281  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  nnssn0s  28326  tgisline  28635  upgrss  29105  frgrwopreg2  30338  difxp1ss  32541  difxp2ss  32542  xrge00  33017  symgcom2  33104  pmtrcnel  33109  pmtrcnel2  33110  pmtrcnelor  33111  cycpmrn  33163  tocyccntz  33164  submatres  33805  madjusmdetlem2  33827  madjusmdetlem3  33828  qtophaus  33835  fsumcvg4  33949  gsumesum  34060  pwsiga  34131  sigainb  34137  carsggect  34320  omsmeas  34325  sitgclg  34344  ballotlemfelz  34493  ballotlemfp1  34494  ballotth  34540  cxpcncf1  34610  logdivsqrle  34665  hgt750lemb  34671  kur14lem6  35216  kur14lem7  35217  cvmscld  35278  satfvsucsuc  35370  satfrnmapom  35375  mclsppslem  35588  fundmpss  35767  relsset  35889  limitssson  35912  fnsingle  35920  funimage  35929  cldbnd  36327  clsun  36329  topdifinffinlem  37348  inunissunidif  37376  pibt2  37418  matunitlindflem1  37623  poimirlem8  37635  poimirlem26  37653  poimirlem30  37657  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  voliunnfl  37671  cnambfre  37675  dvtan  37677  dvasin  37711  dvacos  37712  areacirclem4  37718  fdc  37752  divrngcl  37964  isdrngo2  37965  isdrngo3  37966  islsati  38995  hdmap14lem2a  41869  redvmptabs  42390  prjspreln0  42619  prjspvs  42620  prjspeclsp  42622  0prjspnrel  42637  istopclsd  42711  diophin  42783  dnnumch1  43056  deg1mhm  43212  gneispace  44147  inaex  44316  sumnnodd  45645  cncficcgt0  45903  cncfiooicclem1  45908  cxpcncf2  45914  dirkercncflem2  46119  fourierdlem62  46183  fourierdlem66  46187  fourierdlem68  46189  fourierdlem95  46216  etransclem24  46273  etransclem44  46293  gsumge0cl  46386  sge0fodjrnlem  46431  carageniuncllem1  46536  smfresal  46803  dfnbgrss  47838  dfnbgrss2  47845  lindslinindimp2lem2  48376  iscnrm3rlem2  48838  amgmlemALT  49322