Theorem difss 4086

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

Syntax hints:   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-ss 3919

This theorem is referenced by:  difssd  4087  difss2  4088  ssdifss  4090  0dif  4355  disj4  4409  difsnpss  4759  unidif  4893  iunxdif2  5002  difexg  5267  difelpw  5292  reldif  5755  cnvdif  6090  difxp  6111  frpoind  6289  tz7.7  6332  fresaun  6694  fresaunres2  6695  resdif  6784  fndmdif  6975  tfi  7783  peano5  7823  oelim2  8510  swoer  8653  swoord1  8654  swoord2  8655  ralxpmap  8820  boxcutc  8865  undom  8978  domunsncan  8990  sbthlem2  9001  sbthlem4  9003  sbthlem5  9004  limenpsi  9065  diffi  9084  php3  9118  frfi  9169  fofinf1o  9216  ixpfi2  9234  elfiun  9314  marypha1lem  9317  wemapso  9437  infdifsn  9547  cantnflem2  9580  frind  9643  frr1  9652  dfac8alem  9920  acnnum  9943  inffien  9954  kmlem5  10046  infdif  10099  infdif2  10100  ackbij1lem18  10127  fictb  10135  fin23lem7  10207  fin23lem11  10208  fin23lem28  10231  fin23lem30  10233  compsscnvlem  10261  isf34lem2  10264  compssiso  10265  isf34lem4  10268  fin1a2lem7  10297  axcclem  10348  zornn0g  10396  ttukey2g  10407  pinn  10769  niex  10772  ltsopi  10779  dmaddpi  10781  dmmulpi  10782  lerelxr  11175  mulnzcnf  11763  dflt2  13047  expcl2lem  13980  expclzlem  13990  hashun2  14290  fsumss  15632  fsumless  15703  cvgcmpce  15725  fprodss  15855  rpnnen2lem9  16131  isstruct2  17060  structcnvcnv  17064  strleun  17068  strle1  17069  fsets  17080  mreexexlem2d  17551  gsumpropd2lem  18587  symgfixf1  19350  f1omvdmvd  19356  mvdco  19358  f1omvdconj  19359  pmtrfb  19378  pmtrfconj  19379  symggen  19383  symggen2  19384  psgnunilem1  19406  frgpnabllem2  19787  dprdss  19944  dprd2da  19957  dmdprdsplit2lem  19960  dpjidcl  19973  ablfac1b  19985  ablfac1eu  19988  isdomn3  20631  isdrng2  20659  drngmclOLD  20667  drngid2  20668  isdrngd  20681  isdrngdOLD  20683  cntzsdrg  20718  subdrgint  20719  cnmgpid  21367  cnmsubglem  21368  xrs1mnd  21378  xrs10  21379  xrs1cmn  21380  xrge0subm  21381  xrge0cmn  21382  expghm  21413  dsmmfi  21676  islinds2  21751  lindsind2  21757  lindfrn  21759  islindf4  21776  psdmul  22082  mdetdiaglem  22514  mdetrsca2  22520  mdetrlin2  22523  mdetralt  22524  mdetunilem5  22532  mdetunilem9  22536  maducoeval2  22556  smadiadetglem1  22587  isopn2  22948  ntrval2  22967  ntrdif  22968  clsdif  22969  ntrss  22971  cmclsopn  22978  discld  23005  mretopd  23008  lpsscls  23057  restntr  23098  cmpcld  23318  2ndcsep  23375  1stccnp  23378  llycmpkgen2  23466  1stckgen  23470  txkgen  23568  qtopcld  23629  qtopcmap  23635  kqdisj  23648  isufil2  23824  ufileu  23835  filufint  23836  fixufil  23838  cfinufil  23844  ufilen  23846  fin1aufil  23848  supnfcls  23936  flimfnfcls  23944  alexsublem  23960  alexsubALTlem3  23965  cldsubg  24027  imasdsf1olem  24289  recld2  24731  sszcld  24734  xrge0gsumle  24750  divcnOLD  24785  divcn  24787  cdivcncf  24842  bcth3  25259  ismbl2  25456  cmmbl  25463  nulmbl  25464  nulmbl2  25465  unmbl  25466  voliunlem1  25479  voliunlem2  25480  ioombl1lem4  25490  ioombl1  25491  uniioombllem3  25514  mbfss  25575  itg1cl  25614  itg1ge0  25615  i1f0  25616  i1f1  25619  i1fmul  25625  itg1addlem4  25628  itg1mulc  25633  itg10a  25639  itg1ge0a  25640  itg1climres  25643  itg2cnlem1  25690  itgioo  25745  itgsplitioo  25767  limcdif  25805  ellimc2  25806  ellimc3  25808  limcflflem  25809  limcflf  25810  limcmo  25811  limcresi  25814  dvreslem  25838  dvres2lem  25839  dvidlem  25844  dvcnp2  25849  dvcnp2OLD  25850  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcobr  25877  dvcobrOLD  25878  dvrec  25887  dvcnvlem  25908  lhop1lem  25946  lhop  25949  tdeglem4  25993  deg1n0ima  26022  aacjcl  26263  taylthlem2  26310  taylthlem2OLD  26311  abelth  26379  logcnlem5  26583  dvlog2  26590  efopnlem2  26594  dvcncxp1  26680  dvcnsqrt  26681  cxpcn2  26684  sqrtcn  26688  efrlim  26907  efrlimOLD  26908  jensen  26927  amgm  26929  lgamgulmlem2  26968  lgamucov  26976  wilthlem2  27007  dchrelbas2  27176  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem3  27458  dchrisum0  27459  nnssn0s  28251  tgisline  28606  upgrss  29067  frgrwopreg2  30297  difxp1ss  32500  difxp2ss  32501  xrge00  32993  symgcom2  33051  pmtrcnel  33056  pmtrcnel2  33057  pmtrcnelor  33058  cycpmrn  33110  tocyccntz  33111  submatres  33817  madjusmdetlem2  33839  madjusmdetlem3  33840  qtophaus  33847  fsumcvg4  33961  gsumesum  34070  pwsiga  34141  sigainb  34147  carsggect  34329  omsmeas  34334  sitgclg  34353  ballotlemfelz  34502  ballotlemfp1  34503  ballotth  34549  cxpcncf1  34606  logdivsqrle  34661  hgt750lemb  34667  fineqvnttrclse  35142  kur14lem6  35253  kur14lem7  35254  cvmscld  35315  satfvsucsuc  35407  satfrnmapom  35412  mclsppslem  35625  fundmpss  35809  relsset  35928  limitssson  35951  fnsingle  35959  funimage  35968  cldbnd  36366  clsun  36368  topdifinffinlem  37387  inunissunidif  37415  pibt2  37457  matunitlindflem1  37662  poimirlem8  37674  poimirlem26  37692  poimirlem30  37696  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  voliunnfl  37710  cnambfre  37714  dvtan  37716  dvasin  37750  dvacos  37751  areacirclem4  37757  fdc  37791  divrngcl  38003  isdrngo2  38004  isdrngo3  38005  islsati  39039  hdmap14lem2a  41912  redvmptabs  42399  prjspreln0  42648  prjspvs  42649  prjspeclsp  42651  0prjspnrel  42666  istopclsd  42739  diophin  42811  dnnumch1  43083  deg1mhm  43239  gneispace  44173  inaex  44336  sumnnodd  45676  cncficcgt0  45932  cncfiooicclem1  45937  cxpcncf2  45943  dirkercncflem2  46148  fourierdlem62  46212  fourierdlem66  46216  fourierdlem68  46218  fourierdlem95  46245  etransclem24  46302  etransclem44  46322  gsumge0cl  46415  sge0fodjrnlem  46460  carageniuncllem1  46565  smfresal  46832  dfnbgrss  47889  dfnbgrss2  47896  lindslinindimp2lem2  48497  iscnrm3rlem2  48978  amgmlemALT  49841