Theorem difss 4075

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

This proof depends on syntax axioms:   ⊆ wss 3900   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050

This theorem is used by:  difssd  4076  difss2  4077  ssdifss  4079  0dif  4359  disj4  4415  difsnpss  4770  unidif  4906  iunxdif2  5015  difexg  5296  difelpw  5320  reldif  5800  cnvdif  6150  difxp  6171  frpoind  6369  tz7.7  6412  fundif  6616  fresaun  6781  fresaunres2  6782  resdif  6874  fndmdif  7070  tfi  7896  peano5  7937  oelim2  8640  swoer  8785  swoord1  8786  swoord2  8787  ralxpmap  8960  boxcutc  9005  undom  9120  domunsncan  9132  sbthlem2  9143  sbthlem4  9145  sbthlem5  9146  limenpsi  9207  diffi  9226  php3  9260  frfi  9312  fofinf1o  9357  ixpfi2  9375  elfiun  9457  marypha1lem  9460  wemapso  9580  infdifsn  9693  cantnflem2  9726  frind  9789  frr1  9798  dfac8alem  10145  acnnum  10168  inffien  10179  kmlem5  10270  infdif  10323  infdif2  10324  ackbij1lem18  10351  fictb  10359  fin23lem7  10431  fin23lem11  10432  fin23lem28  10455  fin23lem30  10457  compsscnvlem  10485  isf34lem2  10488  compssiso  10489  isf34lem4  10492  fin1a2lem7  10521  axcclem  10572  zornn0g  10620  ttukey2g  10631  pinn  11000  niex  11003  ltsopi  11010  dmaddpi  11012  dmmulpi  11013  lerelxr  11409  mulnzcnf  12000  dflt2  13315  expcl2lem  14254  expclzlem  14264  hashun2  14566  fsumss  15932  fsumless  16004  cvgcmpce  16026  fprodss  16156  rpnnen2lem9  16431  isstruct2  17368  structcnvcnv  17372  strleun  17376  strle1  17377  fsets  17388  mreexexlem2d  17860  gsumpropd2lem  18909  symgfixf1  19693  f1omvdmvd  19699  mvdco  19701  f1omvdconj  19702  pmtrfb  19721  pmtrfconj  19722  symggen  19726  symggen2  19727  psgnunilem1  19749  frgpnabllem2  20130  dprdss  20287  dprd2da  20300  dmdprdsplit2lem  20303  dpjidcl  20316  ablfac1b  20328  ablfac1eu  20331  isdomn3  21008  isdrng2  21039  isdrng3lem0  21046  isdrng3lem2  21048  isdrng5  21050  drngid2  21052  isdrngd  21064  isdrngdOLD  21066  cntzsdrg  21101  subdrgint  21102  prmidlsubm  21685  cnmgpid  21779  cnmsubglem  21780  xrs1mnd  21790  xrs10  21791  xrs1cmn  21792  xrge0subm  21793  xrge0cmn  21794  expghm  21825  dsmmfi  22088  islinds2  22163  lindsind2  22169  lindfrn  22171  islindf4  22188  psdmul  22531  mdetdiaglem  22957  mdetrsca2  22963  mdetrlin2  22966  mdetralt  22967  mdetunilem5  22975  mdetunilem9  22979  maducoeval2  22999  smadiadetglem1  23030  matunitlindflem1  23038  isopn2  23394  ntrval2  23413  ntrdif  23414  clsdif  23415  ntrss  23417  cmclsopn  23424  discld  23451  mretopd  23454  lpsscls  23503  restntr  23544  cmpcld  23764  2ndcsep  23822  1stccnp  23825  llycmpkgen2  23913  1stckgen  23917  txkgen  24015  qtopcld  24076  qtopcmap  24082  kqdisj  24095  isufil2  24271  ufileu  24282  filufint  24283  fixufil  24285  cfinufil  24291  ufilen  24293  fin1aufil  24295  supnfcls  24383  flimfnfcls  24391  alexsublem  24407  alexsubALTlem3  24412  cldsubg  24474  imasdsf1olem  24736  recld2  25178  sszcld  25181  xrge0gsumle  25197  divcn  25233  cdivcncf  25286  bcth3  25696  ismbl2  25892  cmmbl  25899  nulmbl  25900  nulmbl2  25901  unmbl  25902  voliunlem1  25915  voliunlem2  25916  ioombl1lem4  25926  ioombl1  25927  uniioombllem3  25950  mbfss  26011  itg1cl  26050  itg1ge0  26051  i1f0  26052  i1f1  26055  i1fmul  26061  itg1addlem4  26064  itg1mulc  26069  itg10a  26075  itg1ge0a  26076  itg1climres  26079  itg2cnlem1  26126  itgioo  26180  itgsplitioo  26202  limcdif  26240  ellimc2  26241  ellimc3  26243  limcflflem  26244  limcflf  26245  limcmo  26246  limcresi  26249  dvreslem  26273  dvres2lem  26274  dvidlem  26279  dvcnp2  26284  dvaddbr  26302  dvmulbr  26303  dvcobr  26310  dvrec  26319  dvcnvlem  26340  lhop1lem  26377  lhop  26380  tdeglem4  26422  deg1n0ima  26451  aacjcl  26700  taylthlem2  26747  abelth  26814  logcnlem5  27020  dvlog2  27027  efopnlem2  27031  dvcncxp1  27117  dvcnsqrt  27118  cxpcn2  27120  sqrtcn  27124  efrlim  27343  jensen  27362  amgm  27364  lgamgulmlem2  27403  lgamucov  27411  wilthlem2  27442  dchrelbas2  27610  rpvmasum2  27885  dchrisum0re  27886  dchrisum0lem3  27892  dchrisum0  27893  nnssn0s  28753  tgisline  29141  upgrss  29712  frgrwopreg2  30966  difxp1ss  33206  difxp2ss  33207  xrge00  33664  symgcom2  33734  pmtrcnel  33739  pmtrcnel2  33740  pmtrcnelor  33741  cycpmrn  33793  tocyccntz  33794  evlextv  34278  vietalem  34315  submatres  34542  madjusmdetlem2  34564  madjusmdetlem3  34565  qtophaus  34572  fsumcvg4  34686  gsumesum  34795  pwsiga  34866  sigainb  34873  carsggect  35054  omsmeas  35059  sitgclg  35078  ballotlemfelz  35227  ballotlemfp1  35228  ballotth  35274  cxpcncf1  35328  logdivsqrle  35383  hgt750lemb  35389  fineqvnttrclse  35926  kur14lem6  36177  kur14lem7  36178  cvmscld  36239  satfvsucsuc  36331  satfrnmapom  36336  mclsppslem  36549  fundmpss  36740  relsset  36858  limitssson  36881  fnsingle  36889  funimage  36898  cldbnd  37322  clsun  37324  topdifinffinlem  38531  inunissunidif  38559  pibt2  38601  poimirlem8  38807  poimirlem26  38825  poimirlem30  38829  mblfinlem3  38838  mblfinlem4  38839  ismblfin  38840  voliunnfl  38843  cnambfre  38847  dvtan  38849  dvasin  38883  dvacos  38884  areacirclem4  38890  fdc  38938  divrngcl  39150  isdrngo2  39151  isdrngo3  39152  islsati  40310  hdmap14lem2a  43183  redvmptabs  43671  prjspreln0  43897  prjspvs  43898  prjspeclsp  43900  frlmnzcoordcl2  43916  prjspnnorm  43921  0prjspnrel  43923  istopclsd  43971  diophin  44043  dnnumch1  44311  deg1mhm  44457  gneispace  45389  inaex  45536  sumnnodd  46909  cncficcgt0  47165  cncfiooicclem1  47170  cxpcncf2  47176  dirkercncflem2  47381  fourierdlem62  47445  fourierdlem66  47449  fourierdlem68  47451  fourierdlem95  47478  etransclem24  47535  etransclem44  47555  gsumge0cl  47648  sge0fodjrnlem  47693  carageniuncllem1  47798  smfresal  48065  dfnbgrss  49217  dfnbgrss2  49224  lindslinindimp2lem2  49896  iscnrm3rlem2  50380  amgmlemALT  51410