Theorem difss 4072

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

This proof depends on syntax axioms:   ⊆ wss 3895   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047

This theorem is used by:  difssd  4073  difss2  4074  ssdifss  4076  0dif  4355  disj4  4411  difsnpss  4766  unidif  4902  iunxdif2  5011  difexg  5290  difelpw  5314  reldif  5792  cnvdif  6133  difxp  6154  frpoind  6345  tz7.7  6388  fresaun  6754  fresaunres2  6755  resdif  6847  fndmdif  7042  tfi  7865  peano5  7906  oelim2  8608  swoer  8753  swoord1  8754  swoord2  8755  ralxpmap  8928  boxcutc  8973  undom  9088  domunsncan  9100  sbthlem2  9111  sbthlem4  9113  sbthlem5  9114  limenpsi  9175  diffi  9194  php3  9228  frfi  9280  fofinf1o  9325  ixpfi2  9343  elfiun  9426  marypha1lem  9429  wemapso  9549  infdifsn  9662  cantnflem2  9695  frind  9758  frr1  9767  dfac8alem  10112  acnnum  10135  inffien  10146  kmlem5  10237  infdif  10290  infdif2  10291  ackbij1lem18  10318  fictb  10326  fin23lem7  10398  fin23lem11  10399  fin23lem28  10422  fin23lem30  10424  compsscnvlem  10452  isf34lem2  10455  compssiso  10456  isf34lem4  10459  fin1a2lem7  10488  axcclem  10539  zornn0g  10587  ttukey2g  10598  pinn  10967  niex  10970  ltsopi  10977  dmaddpi  10979  dmmulpi  10980  lerelxr  11376  mulnzcnf  11966  dflt2  13281  expcl2lem  14220  expclzlem  14230  hashun2  14531  fsumss  15897  fsumless  15969  cvgcmpce  15991  fprodss  16121  rpnnen2lem9  16396  isstruct2  17333  structcnvcnv  17337  strleun  17341  strle1  17342  fsets  17353  mreexexlem2d  17825  gsumpropd2lem  18874  symgfixf1  19657  f1omvdmvd  19663  mvdco  19665  f1omvdconj  19666  pmtrfb  19685  pmtrfconj  19686  symggen  19690  symggen2  19691  psgnunilem1  19713  frgpnabllem2  20094  dprdss  20251  dprd2da  20264  dmdprdsplit2lem  20267  dpjidcl  20280  ablfac1b  20292  ablfac1eu  20295  isdomn3  20972  isdrng2  21003  isdrng3lem0  21010  isdrng3lem2  21012  isdrng5  21014  drngid2  21016  isdrngd  21028  isdrngdOLD  21030  cntzsdrg  21065  subdrgint  21066  prmidlsubm  21649  cnmgpid  21741  cnmsubglem  21742  xrs1mnd  21752  xrs10  21753  xrs1cmn  21754  xrge0subm  21755  xrge0cmn  21756  expghm  21787  dsmmfi  22050  islinds2  22125  lindsind2  22131  lindfrn  22133  islindf4  22150  psdmul  22493  mdetdiaglem  22919  mdetrsca2  22925  mdetrlin2  22928  mdetralt  22929  mdetunilem5  22937  mdetunilem9  22941  maducoeval2  22961  smadiadetglem1  22992  matunitlindflem1  23000  isopn2  23356  ntrval2  23375  ntrdif  23376  clsdif  23377  ntrss  23379  cmclsopn  23386  discld  23413  mretopd  23416  lpsscls  23465  restntr  23506  cmpcld  23726  2ndcsep  23784  1stccnp  23787  llycmpkgen2  23875  1stckgen  23879  txkgen  23977  qtopcld  24038  qtopcmap  24044  kqdisj  24057  isufil2  24233  ufileu  24244  filufint  24245  fixufil  24247  cfinufil  24253  ufilen  24255  fin1aufil  24257  supnfcls  24345  flimfnfcls  24353  alexsublem  24369  alexsubALTlem3  24374  cldsubg  24436  imasdsf1olem  24698  recld2  25140  sszcld  25143  xrge0gsumle  25159  divcn  25195  cdivcncf  25248  bcth3  25658  ismbl2  25854  cmmbl  25861  nulmbl  25862  nulmbl2  25863  unmbl  25864  voliunlem1  25877  voliunlem2  25878  ioombl1lem4  25888  ioombl1  25889  uniioombllem3  25912  mbfss  25973  itg1cl  26012  itg1ge0  26013  i1f0  26014  i1f1  26017  i1fmul  26023  itg1addlem4  26026  itg1mulc  26031  itg10a  26037  itg1ge0a  26038  itg1climres  26041  itg2cnlem1  26088  itgioo  26142  itgsplitioo  26164  limcdif  26202  ellimc2  26203  ellimc3  26205  limcflflem  26206  limcflf  26207  limcmo  26208  limcresi  26211  dvreslem  26235  dvres2lem  26236  dvidlem  26241  dvcnp2  26246  dvaddbr  26264  dvmulbr  26265  dvcobr  26272  dvrec  26281  dvcnvlem  26302  lhop1lem  26339  lhop  26342  tdeglem4  26384  deg1n0ima  26413  aacjcl  26660  taylthlem2  26707  abelth  26774  logcnlem5  26980  dvlog2  26987  efopnlem2  26991  dvcncxp1  27077  dvcnsqrt  27078  cxpcn2  27080  sqrtcn  27084  efrlim  27303  jensen  27322  amgm  27324  lgamgulmlem2  27363  lgamucov  27371  wilthlem2  27402  dchrelbas2  27570  rpvmasum2  27845  dchrisum0re  27846  dchrisum0lem3  27852  dchrisum0  27853  nnssn0s  28713  tgisline  29101  upgrss  29672  frgrwopreg2  30926  difxp1ss  33166  difxp2ss  33167  xrge00  33622  symgcom2  33692  pmtrcnel  33697  pmtrcnel2  33698  pmtrcnelor  33699  cycpmrn  33751  tocyccntz  33752  evlextv  34221  vietalem  34258  submatres  34485  madjusmdetlem2  34507  madjusmdetlem3  34508  qtophaus  34515  fsumcvg4  34629  gsumesum  34738  pwsiga  34809  sigainb  34816  carsggect  34997  omsmeas  35002  sitgclg  35021  ballotlemfelz  35170  ballotlemfp1  35171  ballotth  35217  cxpcncf1  35271  logdivsqrle  35326  hgt750lemb  35332  fineqvnttrclse  35849  kur14lem6  36063  kur14lem7  36064  cvmscld  36125  satfvsucsuc  36217  satfrnmapom  36222  mclsppslem  36435  fundmpss  36625  relsset  36743  limitssson  36766  fnsingle  36774  funimage  36783  cldbnd  37207  clsun  37209  topdifinffinlem  38364  inunissunidif  38392  pibt2  38434  poimirlem8  38640  poimirlem26  38658  poimirlem30  38662  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  voliunnfl  38676  cnambfre  38680  dvtan  38682  dvasin  38716  dvacos  38717  areacirclem4  38723  fdc  38773  divrngcl  38985  isdrngo2  38986  isdrngo3  38987  islsati  40145  hdmap14lem2a  43018  redvmptabs  43505  prjspreln0  43731  prjspvs  43732  prjspeclsp  43734  frlmnzcoordcl2  43750  prjspnnorm  43755  0prjspnrel  43757  istopclsd  43805  diophin  43877  dnnumch1  44145  deg1mhm  44296  gneispace  45228  inaex  45375  sumnnodd  46736  cncficcgt0  46992  cncfiooicclem1  46997  cxpcncf2  47003  dirkercncflem2  47208  fourierdlem62  47272  fourierdlem66  47276  fourierdlem68  47278  fourierdlem95  47305  etransclem24  47362  etransclem44  47382  gsumge0cl  47475  sge0fodjrnlem  47520  carageniuncllem1  47625  smfresal  47892  dfnbgrss  49044  dfnbgrss2  49051  lindslinindimp2lem2  49665  iscnrm3rlem2  50149  amgmlemALT  51157