Theorem difss 4127

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

Syntax hints:   ∖ cdif 3941   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-dif 3947  df-in 3951  df-ss 3961

This theorem is referenced by:  difssd  4128  difss2  4129  ssdifss  4131  0dif  4397  disj4  4454  difsnpss  4806  unidif  4940  iunxdif2  5050  difexg  5323  difelpw  5347  reldif  5811  cnvdif  6142  difxp  6162  frpoind  6342  wfiOLD  6351  tz7.7  6389  fresaun  6762  fresaunres2  6763  resdif  6854  fndmdif  7045  tfi  7851  peano5  7893  peano5OLD  7894  wfrlem16OLD  8338  oelim2  8609  swoer  8748  swoord1  8749  swoord2  8750  ralxpmap  8906  boxcutc  8951  undom  9075  undomOLD  9076  domunsncan  9088  sbthlem2  9100  sbthlem4  9102  sbthlem5  9103  limenpsi  9168  diffi  9195  php3  9228  phplem2OLD  9234  php3OLD  9240  frfi  9304  fofinf1o  9343  ixpfi2  9366  elfiun  9445  marypha1lem  9448  wemapso  9566  infdifsn  9672  cantnflem2  9705  frind  9765  frr1  9774  dfac8alem  10044  acnnum  10067  inffien  10078  kmlem5  10169  infdif  10224  infdif2  10225  ackbij1lem18  10252  fictb  10260  fin23lem7  10331  fin23lem11  10332  fin23lem28  10355  fin23lem30  10357  compsscnvlem  10385  isf34lem2  10388  compssiso  10389  isf34lem4  10392  fin1a2lem7  10421  axcclem  10472  zornn0g  10520  ttukey2g  10531  pinn  10893  niex  10896  ltsopi  10903  dmaddpi  10905  dmmulpi  10906  lerelxr  11299  mulnzcnf  11882  dflt2  13151  expcl2lem  14062  expclzlem  14072  hashun2  14366  fsumss  15695  fsumless  15766  cvgcmpce  15788  fprodss  15916  rpnnen2lem9  16190  isstruct2  17109  structcnvcnv  17113  strleun  17117  strle1  17118  fsets  17129  mreexexlem2d  17616  gsumpropd2lem  18630  symgfixf1  19383  f1omvdmvd  19389  mvdco  19391  f1omvdconj  19392  pmtrfb  19411  pmtrfconj  19412  symggen  19416  symggen2  19417  psgnunilem1  19439  frgpnabllem2  19820  dprdss  19977  dprd2da  19990  dmdprdsplit2lem  19993  dpjidcl  20006  ablfac1b  20018  ablfac1eu  20021  isdrng2  20627  drngmcl  20630  drngid2  20634  isdrngd  20646  isdrngdOLD  20648  cntzsdrg  20679  subdrgint  20680  xrs1mnd  21324  xrs10  21325  xrs1cmn  21326  xrge0subm  21327  xrge0cmn  21328  cnmgpid  21349  cnmsubglem  21350  expghm  21388  dsmmfi  21659  islinds2  21734  lindsind2  21740  lindfrn  21742  islindf4  21759  psdmul  22077  mdetdiaglem  22487  mdetrsca2  22493  mdetrlin2  22496  mdetralt  22497  mdetunilem5  22505  mdetunilem9  22509  maducoeval2  22529  smadiadetglem1  22560  isopn2  22923  ntrval2  22942  ntrdif  22943  clsdif  22944  ntrss  22946  cmclsopn  22953  discld  22980  mretopd  22983  lpsscls  23032  restntr  23073  cmpcld  23293  2ndcsep  23350  1stccnp  23353  llycmpkgen2  23441  1stckgen  23445  txkgen  23543  qtopcld  23604  qtopcmap  23610  kqdisj  23623  isufil2  23799  ufileu  23810  filufint  23811  fixufil  23813  cfinufil  23819  ufilen  23821  fin1aufil  23823  supnfcls  23911  flimfnfcls  23919  alexsublem  23935  alexsubALTlem3  23940  cldsubg  24002  imasdsf1olem  24266  recld2  24717  sszcld  24720  xrge0gsumle  24736  divcnOLD  24771  divcn  24773  cdivcncf  24828  bcth3  25246  ismbl2  25443  cmmbl  25450  nulmbl  25451  nulmbl2  25452  unmbl  25453  voliunlem1  25466  voliunlem2  25467  ioombl1lem4  25477  ioombl1  25478  uniioombllem3  25501  mbfss  25562  itg1cl  25601  itg1ge0  25602  i1f0  25603  i1f1  25606  i1fmul  25612  itg1addlem4  25615  itg1addlem4OLD  25616  itg1mulc  25621  itg10a  25627  itg1ge0a  25628  itg1climres  25631  itg2cnlem1  25678  itgioo  25732  itgsplitioo  25754  limcdif  25792  ellimc2  25793  ellimc3  25795  limcflflem  25796  limcflf  25797  limcmo  25798  limcresi  25801  dvreslem  25825  dvres2lem  25826  dvidlem  25831  dvcnp2  25836  dvcnp2OLD  25837  dvaddbr  25855  dvmulbr  25856  dvmulbrOLD  25857  dvcobr  25864  dvcobrOLD  25865  dvrec  25874  dvcnvlem  25895  lhop1lem  25933  lhop  25936  tdeglem4  25982  tdeglem4OLD  25983  deg1n0ima  26012  aacjcl  26249  taylthlem2  26296  taylthlem2OLD  26297  abelth  26365  logcnlem5  26567  dvlog2  26574  efopnlem2  26578  dvcncxp1  26664  dvcnsqrt  26665  cxpcn2  26668  sqrtcn  26672  efrlim  26888  efrlimOLD  26889  jensen  26908  amgm  26910  lgamgulmlem2  26949  lgamucov  26957  wilthlem2  26988  dchrelbas2  27157  rpvmasum2  27432  dchrisum0re  27433  dchrisum0lem3  27439  dchrisum0  27440  nnssn0s  28180  tgisline  28418  upgrss  28888  frgrwopreg2  30116  difxp1ss  32304  difxp2ss  32305  xrge00  32724  symgcom2  32785  pmtrcnel  32790  pmtrcnel2  32791  pmtrcnelor  32792  cycpmrn  32842  tocyccntz  32843  submatres  33343  madjusmdetlem2  33365  madjusmdetlem3  33366  qtophaus  33373  fsumcvg4  33487  gsumesum  33614  pwsiga  33685  sigainb  33691  carsggect  33874  omsmeas  33879  sitgclg  33898  ballotlemfelz  34046  ballotlemfp1  34047  ballotth  34093  cxpcncf1  34163  logdivsqrle  34218  hgt750lemb  34224  kur14lem6  34757  kur14lem7  34758  cvmscld  34819  satfvsucsuc  34911  satfrnmapom  34916  mclsppslem  35129  fundmpss  35298  relsset  35420  limitssson  35443  fnsingle  35451  funimage  35460  cldbnd  35746  clsun  35748  topdifinffinlem  36762  inunissunidif  36790  pibt2  36832  matunitlindflem1  37024  poimirlem8  37036  poimirlem26  37054  poimirlem30  37058  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  voliunnfl  37072  cnambfre  37076  dvtan  37078  dvasin  37112  dvacos  37113  areacirclem4  37119  fdc  37153  divrngcl  37365  isdrngo2  37366  isdrngo3  37367  islsati  38403  hdmap14lem2a  41277  prjspreln0  41955  prjspvs  41956  prjspeclsp  41958  0prjspnrel  41973  istopclsd  42042  diophin  42114  dnnumch1  42390  isdomn3  42549  deg1mhm  42551  gneispace  43487  inaex  43657  sumnnodd  44941  cncficcgt0  45199  cncfiooicclem1  45204  cxpcncf2  45210  dirkercncflem2  45415  fourierdlem62  45479  fourierdlem66  45483  fourierdlem68  45485  fourierdlem95  45512  etransclem24  45569  etransclem44  45589  gsumge0cl  45682  sge0fodjrnlem  45727  carageniuncllem1  45832  smfresal  46099  lindslinindimp2lem2  47450  iscnrm3rlem2  47883  amgmlemALT  48159