Theorem difss 4108

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

Syntax hints:   ∖ cdif 3933   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  difssd  4109  difss2  4110  ssdifss  4112  0dif  4355  disj4  4408  difsnpss  4740  unidif  4872  iunxdif2  4977  difexg  5231  difelpw  5252  reldif  5688  cnvdif  6002  difxp  6021  wfi  6181  tz7.7  6217  fresaun  6549  fresaunres2  6550  resdif  6635  fndmdif  6812  tfi  7568  peano5  7605  wfrlem16  7970  oelim2  8221  swoer  8319  swoord1  8320  swoord2  8321  ralxpmap  8460  boxcutc  8505  undom  8605  domunsncan  8617  sbthlem2  8628  sbthlem4  8630  sbthlem5  8631  limenpsi  8692  phplem2  8697  php3  8703  diffi  8750  frfi  8763  fofinf1o  8799  ixpfi2  8822  elfiun  8894  marypha1lem  8897  wemapso  9015  infdifsn  9120  cantnflem2  9153  dfac8alem  9455  acnnum  9478  inffien  9489  kmlem5  9580  infdif  9631  infdif2  9632  ackbij1lem18  9659  fictb  9667  fin23lem7  9738  fin23lem11  9739  fin23lem28  9762  fin23lem30  9764  compsscnvlem  9792  isf34lem2  9795  compssiso  9796  isf34lem4  9799  fin1a2lem7  9828  axcclem  9879  zornn0g  9927  ttukey2g  9938  pinn  10300  niex  10303  ltsopi  10310  dmaddpi  10312  dmmulpi  10313  lerelxr  10704  mulnzcnopr  11286  dflt2  12542  expcl2lem  13442  expclzlem  13454  hashun2  13745  fsumss  15082  fsumless  15151  cvgcmpce  15173  fprodss  15302  rpnnen2lem9  15575  isstruct2  16493  structcnvcnv  16497  fsets  16516  strleun  16591  strle1  16592  mreexexlem2d  16916  gsumpropd2lem  17889  symgfixf1  18565  f1omvdmvd  18571  mvdco  18573  f1omvdconj  18574  pmtrfb  18593  pmtrfconj  18594  symggen  18598  symggen2  18599  psgnunilem1  18621  frgpnabllem2  18994  dprdss  19151  dprd2da  19164  dmdprdsplit2lem  19167  dpjidcl  19180  ablfac1b  19192  ablfac1eu  19195  isdrng2  19512  drngmcl  19515  drngid2  19518  isdrngd  19527  cntzsdrg  19581  subdrgint  19582  xrs1mnd  20583  xrs10  20584  xrs1cmn  20585  xrge0subm  20586  xrge0cmn  20587  cnmgpid  20607  cnmsubglem  20608  expghm  20643  dsmmfi  20882  islinds2  20957  lindsind2  20963  lindfrn  20965  islindf4  20982  mdetdiaglem  21207  mdetrsca2  21213  mdetrlin2  21216  mdetralt  21217  mdetunilem5  21225  mdetunilem9  21229  maducoeval2  21249  smadiadetglem1  21280  isopn2  21640  ntrval2  21659  ntrdif  21660  clsdif  21661  ntrss  21663  cmclsopn  21670  discld  21697  mretopd  21700  lpsscls  21749  restntr  21790  cmpcld  22010  2ndcsep  22067  1stccnp  22070  llycmpkgen2  22158  1stckgen  22162  txkgen  22260  qtopcld  22321  qtopcmap  22327  kqdisj  22340  isufil2  22516  ufileu  22527  filufint  22528  fixufil  22530  cfinufil  22536  ufilen  22538  fin1aufil  22540  supnfcls  22628  flimfnfcls  22636  alexsublem  22652  alexsubALTlem3  22657  cldsubg  22719  imasdsf1olem  22983  recld2  23422  sszcld  23425  xrge0gsumle  23441  divcn  23476  cdivcncf  23525  bcth3  23934  ismbl2  24128  cmmbl  24135  nulmbl  24136  nulmbl2  24137  unmbl  24138  voliunlem1  24151  voliunlem2  24152  ioombl1lem4  24162  ioombl1  24163  uniioombllem3  24186  mbfss  24247  itg1cl  24286  itg1ge0  24287  i1f0  24288  i1f1  24291  i1fmul  24297  itg1addlem4  24300  itg1mulc  24305  itg10a  24311  itg1ge0a  24312  itg1climres  24315  itg2cnlem1  24362  itgioo  24416  itgsplitioo  24438  limcdif  24474  ellimc2  24475  ellimc3  24477  limcflflem  24478  limcflf  24479  limcmo  24480  limcresi  24483  dvreslem  24507  dvres2lem  24508  dvidlem  24513  dvcnp2  24517  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvrec  24552  dvcnvlem  24573  lhop1lem  24610  lhop  24613  tdeglem4  24654  deg1n0ima  24683  aacjcl  24916  taylthlem2  24962  abelth  25029  logcnlem5  25229  dvlog2  25236  efopnlem2  25240  dvcncxp1  25324  dvcnsqrt  25325  cxpcn2  25327  sqrtcn  25331  efrlim  25547  jensen  25566  amgm  25568  lgamgulmlem2  25607  lgamucov  25615  wilthlem2  25646  dchrelbas2  25813  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem3  26095  dchrisum0  26096  tgisline  26413  upgrss  26873  frgrwopreg2  28098  difxp1ss  30282  difxp2ss  30283  xrge00  30673  symgcom2  30728  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  cycpmrn  30785  tocyccntz  30786  submatres  31071  madjusmdetlem2  31093  madjusmdetlem3  31094  qtophaus  31100  fsumcvg4  31193  gsumesum  31318  pwsiga  31389  sigainb  31395  carsggect  31576  omsmeas  31581  sitgclg  31600  ballotlemfelz  31748  ballotlemfp1  31749  ballotth  31795  cxpcncf1  31866  logdivsqrle  31921  hgt750lemb  31927  kur14lem6  32458  kur14lem7  32459  cvmscld  32520  satfvsucsuc  32612  satfrnmapom  32617  mclsppslem  32830  fundmpss  33009  frpoind  33080  frind  33085  frr1  33144  relsset  33349  limitssson  33372  fnsingle  33380  funimage  33389  cldbnd  33674  clsun  33676  topdifinffinlem  34631  inunissunidif  34659  pibt2  34701  matunitlindflem1  34903  poimirlem8  34915  poimirlem26  34933  poimirlem30  34937  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  voliunnfl  34951  cnambfre  34955  dvtan  34957  dvasin  34993  dvacos  34994  areacirclem4  35000  fdc  35035  divrngcl  35250  isdrngo2  35251  isdrngo3  35252  islsati  36145  hdmap14lem2a  39018  prjspreln0  39308  prjspvs  39309  prjspeclsp  39311  0prjspnrel  39318  istopclsd  39346  diophin  39418  dnnumch1  39693  isdomn3  39853  deg1mhm  39856  gneispace  40533  inaex  40682  sumnnodd  41960  cncficcgt0  42220  cncfiooicclem1  42225  cxpcncf2  42232  dirkercncflem2  42438  fourierdlem62  42502  fourierdlem66  42506  fourierdlem68  42508  fourierdlem95  42535  etransclem24  42592  etransclem44  42612  gsumge0cl  42702  sge0fodjrnlem  42747  carageniuncllem1  42852  smfresal  43112  lindslinindimp2lem2  44563  amgmlemALT  44953