Theorem difss 3434

Description: Subclass relationship for class difference. Exercise 14 of [TakeutiZaring] p. 22. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
difss	|- ( A \ B ) C_ A

Proof of Theorem difss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3429	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 3312	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 3277   C_ wss 3280

This theorem is referenced by:  difssd  3435  difss2  3436  ssdifss  3438  disj4  3636  0dif  3659  uneqdifeq  3676  difsnpss  3901  unidif  4007  iunxdif2  4099  difexg  4311  tz7.7  4567  tfi  4792  peano5  4827  reldif  4953  cnvdif  5237  fresaun  5573  fresaunres2  5574  resdif  5655  fndmdif  5793  difxp  6339  oev  6717  oelim2  6797  swoer  6892  swoord1  6893  swoord2  6894  boxcutc  7064  undom  7155  domunsncan  7167  sbthlem2  7177  sbthlem4  7179  sbthlem5  7180  limenpsi  7241  phplem2  7246  php  7250  php3  7252  pssnn  7286  diffi  7298  frfi  7311  fofinf1o  7346  ixpfi2  7363  elfiun  7393  marypha1lem  7396  wemapso  7476  inf3lem3  7541  infdifsn  7567  cantnflem2  7602  dfac8alem  7866  acnnum  7889  inffien  7900  kmlem5  7990  infdif  8045  infdif2  8046  ackbij1lem18  8073  fictb  8081  fin23lem7  8152  fin23lem11  8153  fin23lem28  8176  fin23lem30  8178  compsscnvlem  8206  isf34lem2  8209  compssiso  8210  isf34lem4  8213  fin1a2lem7  8242  domtriomlem  8278  axcclem  8293  zornn0g  8341  ttukey2g  8352  konigthlem  8399  pinn  8711  niex  8714  ltsopi  8721  dmaddpi  8723  dmmulpi  8724  lerelxr  9097  mulnzcnopr  9624  dflt2  10697  expcl2lem  11348  expclzlem  11360  hashun2  11612  fsumss  12474  fsumless  12530  cvgcmpce  12552  rpnnen2lem9  12777  isstruct2  13433  structcnvcnv  13435  strleun  13514  strle1  13515  mreexexlem2d  13825  frgpnabllem2  15440  dprdss  15542  dprd2da  15555  dmdprdsplit2lem  15558  dpjidcl  15571  ablfac1b  15583  ablfac1eu  15586  isdrng2  15800  drngmcl  15803  drngid2  15806  isdrngd  15815  xrs1mnd  16691  xrs10  16692  xrs1cmn  16693  xrge0subm  16694  xrge0cmn  16695  cnmsubglem  16716  expghm  16732  isopn2  17051  ntrval2  17070  ntrdif  17071  clsdif  17072  ntrss  17074  cmclsopn  17081  cmntrcld  17082  discld  17108  mretopd  17111  lpsscls  17160  restntr  17200  cmpcld  17419  2ndcsep  17475  1stccnp  17478  llycmpkgen2  17535  1stckgen  17539  txkgen  17637  qtopcld  17698  qtopcmap  17704  kqdisj  17717  isufil2  17893  ufileu  17904  filufint  17905  fixufil  17907  cfinufil  17913  ufilen  17915  fin1aufil  17917  supnfcls  18005  flimfnfcls  18013  alexsublem  18028  alexsubALTlem3  18033  cldsubg  18093  imasdsf1olem  18356  recld2  18798  sszcld  18801  xrge0gsumle  18817  divcn  18851  cdivcncf  18900  bcth3  19237  ismbl2  19376  cmmbl  19382  nulmbl  19383  nulmbl2  19384  unmbl  19385  voliunlem1  19397  voliunlem2  19398  ioombl1lem4  19408  ioombl1  19409  uniioombllem3  19430  mbfss  19491  itg1cl  19530  itg1ge0  19531  i1f0  19532  i1f1  19535  i1fmul  19541  itg1addlem4  19544  itg1mulc  19549  itg10a  19555  itg1ge0a  19556  itg1climres  19559  itg2cnlem1  19606  itgioo  19660  itgsplitioo  19682  limcdif  19716  ellimc2  19717  ellimc3  19719  limcflflem  19720  limcflf  19721  limcmo  19722  limcresi  19725  dvreslem  19749  dvres2lem  19750  dvidlem  19755  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvrec  19794  dvcnvlem  19813  lhop1lem  19850  lhop  19853  tdeglem4  19936  deg1n0ima  19965  aacjcl  20197  taylthlem2  20243  abelth  20310  logcnlem5  20490  dvlog2  20497  efopnlem2  20501  cxpcn2  20583  sqrcn  20587  efrlim  20761  jensen  20780  amgm  20782  wilthlem2  20805  dchrelbas2  20974  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  umgrass  21307  xrge00  24161  gsumpropd2lem  24173  gsumesum  24404  pwsiga  24466  sigainb  24472  sibfof  24607  sitgclg  24609  ballotlemfelz  24701  ballotlemfp1  24702  ballotth  24748  lgamgulmlem2  24767  lgamucov  24775  kur14lem6  24850  kur14lem7  24851  cvmscld  24913  fprodss  25227  fundmpss  25336  wfi  25421  frind  25457  wfrlem16  25485  relsset  25642  fnsingle  25672  funimage  25681  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  voliunnfl  26149  cnambfre  26154  areacirclem5  26185  cldbnd  26219  clsun  26221  fdc  26339  divrngcl  26463  isdrngo2  26464  isdrngo3  26465  ralxpmap  26632  istopclsd  26644  diophin  26721  setindtr  26985  dnnumch1  27009  dsmmfi  27072  islinds2  27151  lindsind2  27157  lindfrn  27159  islindf4  27176  f1omvdmvd  27254  mvdco  27256  f1omvdconj  27257  pmtrfb  27274  pmtrfconj  27275  symggen  27279  symggen2  27280  psgnunilem1  27284  cnmsgngrp  27304  psgnghm2  27306  cntzsdrg  27378  isdomn3  27391  deg1mhm  27394  frgrawopreg2  28154  islsati  29477  hdmap14lem2a  32353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294