Theorem difss 4099

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

Syntax hints:   ∖ cdif 3911   ⊆ wss 3914

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  difssd  4100  difss2  4101  ssdifss  4103  0dif  4368  disj4  4422  difsnpss  4771  unidif  4906  iunxdif2  5017  difexg  5284  difelpw  5309  reldif  5778  cnvdif  6116  difxp  6137  frpoind  6315  tz7.7  6358  fresaun  6731  fresaunres2  6732  resdif  6821  fndmdif  7014  tfi  7829  peano5  7869  oelim2  8559  swoer  8702  swoord1  8703  swoord2  8704  ralxpmap  8869  boxcutc  8914  undom  9029  domunsncan  9041  sbthlem2  9052  sbthlem4  9054  sbthlem5  9055  limenpsi  9116  diffi  9139  php3  9173  frfi  9232  fofinf1o  9283  ixpfi2  9301  elfiun  9381  marypha1lem  9384  wemapso  9504  infdifsn  9610  cantnflem2  9643  frind  9703  frr1  9712  dfac8alem  9982  acnnum  10005  inffien  10016  kmlem5  10108  infdif  10161  infdif2  10162  ackbij1lem18  10189  fictb  10197  fin23lem7  10269  fin23lem11  10270  fin23lem28  10293  fin23lem30  10295  compsscnvlem  10323  isf34lem2  10326  compssiso  10327  isf34lem4  10330  fin1a2lem7  10359  axcclem  10410  zornn0g  10458  ttukey2g  10469  pinn  10831  niex  10834  ltsopi  10841  dmaddpi  10843  dmmulpi  10844  lerelxr  11237  mulnzcnf  11824  dflt2  13108  expcl2lem  14038  expclzlem  14048  hashun2  14348  fsumss  15691  fsumless  15762  cvgcmpce  15784  fprodss  15914  rpnnen2lem9  16190  isstruct2  17119  structcnvcnv  17123  strleun  17127  strle1  17128  fsets  17139  mreexexlem2d  17606  gsumpropd2lem  18606  symgfixf1  19367  f1omvdmvd  19373  mvdco  19375  f1omvdconj  19376  pmtrfb  19395  pmtrfconj  19396  symggen  19400  symggen2  19401  psgnunilem1  19423  frgpnabllem2  19804  dprdss  19961  dprd2da  19974  dmdprdsplit2lem  19977  dpjidcl  19990  ablfac1b  20002  ablfac1eu  20005  isdomn3  20624  isdrng2  20652  drngmclOLD  20660  drngid2  20661  isdrngd  20674  isdrngdOLD  20676  cntzsdrg  20711  subdrgint  20712  xrs1mnd  21321  xrs10  21322  xrs1cmn  21323  xrge0subm  21324  xrge0cmn  21325  cnmgpid  21346  cnmsubglem  21347  expghm  21385  dsmmfi  21647  islinds2  21722  lindsind2  21728  lindfrn  21730  islindf4  21747  psdmul  22053  mdetdiaglem  22485  mdetrsca2  22491  mdetrlin2  22494  mdetralt  22495  mdetunilem5  22503  mdetunilem9  22507  maducoeval2  22527  smadiadetglem1  22558  isopn2  22919  ntrval2  22938  ntrdif  22939  clsdif  22940  ntrss  22942  cmclsopn  22949  discld  22976  mretopd  22979  lpsscls  23028  restntr  23069  cmpcld  23289  2ndcsep  23346  1stccnp  23349  llycmpkgen2  23437  1stckgen  23441  txkgen  23539  qtopcld  23600  qtopcmap  23606  kqdisj  23619  isufil2  23795  ufileu  23806  filufint  23807  fixufil  23809  cfinufil  23815  ufilen  23817  fin1aufil  23819  supnfcls  23907  flimfnfcls  23915  alexsublem  23931  alexsubALTlem3  23936  cldsubg  23998  imasdsf1olem  24261  recld2  24703  sszcld  24706  xrge0gsumle  24722  divcnOLD  24757  divcn  24759  cdivcncf  24814  bcth3  25231  ismbl2  25428  cmmbl  25435  nulmbl  25436  nulmbl2  25437  unmbl  25438  voliunlem1  25451  voliunlem2  25452  ioombl1lem4  25462  ioombl1  25463  uniioombllem3  25486  mbfss  25547  itg1cl  25586  itg1ge0  25587  i1f0  25588  i1f1  25591  i1fmul  25597  itg1addlem4  25600  itg1mulc  25605  itg10a  25611  itg1ge0a  25612  itg1climres  25615  itg2cnlem1  25662  itgioo  25717  itgsplitioo  25739  limcdif  25777  ellimc2  25778  ellimc3  25780  limcflflem  25781  limcflf  25782  limcmo  25783  limcresi  25786  dvreslem  25810  dvres2lem  25811  dvidlem  25816  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvrec  25859  dvcnvlem  25880  lhop1lem  25918  lhop  25921  tdeglem4  25965  deg1n0ima  25994  aacjcl  26235  taylthlem2  26282  taylthlem2OLD  26283  abelth  26351  logcnlem5  26555  dvlog2  26562  efopnlem2  26566  dvcncxp1  26652  dvcnsqrt  26653  cxpcn2  26656  sqrtcn  26660  efrlim  26879  efrlimOLD  26880  jensen  26899  amgm  26901  lgamgulmlem2  26940  lgamucov  26948  wilthlem2  26979  dchrelbas2  27148  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  nnssn0s  28214  tgisline  28554  upgrss  29015  frgrwopreg2  30248  difxp1ss  32451  difxp2ss  32452  xrge00  32953  symgcom2  33041  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmrn  33100  tocyccntz  33101  submatres  33796  madjusmdetlem2  33818  madjusmdetlem3  33819  qtophaus  33826  fsumcvg4  33940  gsumesum  34049  pwsiga  34120  sigainb  34126  carsggect  34309  omsmeas  34314  sitgclg  34333  ballotlemfelz  34482  ballotlemfp1  34483  ballotth  34529  cxpcncf1  34586  logdivsqrle  34641  hgt750lemb  34647  kur14lem6  35198  kur14lem7  35199  cvmscld  35260  satfvsucsuc  35352  satfrnmapom  35357  mclsppslem  35570  fundmpss  35754  relsset  35876  limitssson  35899  fnsingle  35907  funimage  35916  cldbnd  36314  clsun  36316  topdifinffinlem  37335  inunissunidif  37363  pibt2  37405  matunitlindflem1  37610  poimirlem8  37622  poimirlem26  37640  poimirlem30  37644  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  voliunnfl  37658  cnambfre  37662  dvtan  37664  dvasin  37698  dvacos  37699  areacirclem4  37705  fdc  37739  divrngcl  37951  isdrngo2  37952  isdrngo3  37953  islsati  38987  hdmap14lem2a  41861  redvmptabs  42348  prjspreln0  42597  prjspvs  42598  prjspeclsp  42600  0prjspnrel  42615  istopclsd  42688  diophin  42760  dnnumch1  43033  deg1mhm  43189  gneispace  44123  inaex  44286  sumnnodd  45628  cncficcgt0  45886  cncfiooicclem1  45891  cxpcncf2  45897  dirkercncflem2  46102  fourierdlem62  46166  fourierdlem66  46170  fourierdlem68  46172  fourierdlem95  46199  etransclem24  46256  etransclem44  46276  gsumge0cl  46369  sge0fodjrnlem  46414  carageniuncllem1  46519  smfresal  46786  dfnbgrss  47852  dfnbgrss2  47859  lindslinindimp2lem2  48448  iscnrm3rlem2  48929  amgmlemALT  49792