Theorem difss 3545

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 3540	. 2 |- ( x e. ( A \ B ) -> x e. A )
2	1	ssriv 3421	1 |- ( A \ B ) C_ A

Syntax hints:   \ cdif 3386   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-dif 3392  df-in 3396  df-ss 3403

This theorem is referenced by:  difssd  3546  difss2  3547  ssdifss  3549  disj4  3791  0dif  3815  uneqdifeq  3832  difsnpss  4087  unidif  4196  iunxdif2  4291  difexg  4513  tz7.7  4818  reldif  5034  cnvdif  5322  difxp  5341  fresaun  5664  fresaunres2  5665  resdif  5744  fndmdif  5893  tfi  6587  peano5  6622  oev  7082  oelim2  7162  swoer  7257  swoord1  7258  swoord2  7259  ralxpmap  7387  boxcutc  7431  undom  7524  domunsncan  7536  sbthlem2  7547  sbthlem4  7549  sbthlem5  7550  limenpsi  7611  phplem2  7616  php  7620  php3  7622  pssnn  7654  diffi  7667  frfi  7680  fofinf1o  7716  ixpfi2  7733  elfiun  7805  marypha1lem  7808  wemapso  7891  inf3lem3  7961  infdifsn  7987  cantnflem2  8022  dfac8alem  8323  acnnum  8346  inffien  8357  kmlem5  8447  infdif  8502  infdif2  8503  ackbij1lem18  8530  fictb  8538  fin23lem7  8609  fin23lem11  8610  fin23lem28  8633  fin23lem30  8635  compsscnvlem  8663  isf34lem2  8666  compssiso  8667  isf34lem4  8670  fin1a2lem7  8699  domtriomlem  8735  axcclem  8750  zornn0g  8798  ttukey2g  8809  konigthlem  8856  pinn  9167  niex  9170  ltsopi  9177  dmaddpi  9179  dmmulpi  9180  lerelxr  9561  mulnzcnopr  10112  dflt2  11275  expcl2lem  12081  expclzlem  12093  hashun2  12354  fsumss  13549  fsumless  13612  cvgcmpce  13634  fprodss  13757  rpnnen2lem9  13958  isstruct2  14643  structcnvcnv  14645  fsets  14662  strleun  14732  strle1  14733  mreexexlem2d  15052  gsumpropd2lem  16017  symgfixf1  16579  f1omvdmvd  16585  mvdco  16587  f1omvdconj  16588  pmtrfb  16607  pmtrfconj  16608  symggen  16612  symggen2  16613  psgnunilem1  16635  frgpnabllem2  16995  dprdss  17189  dprd2da  17204  dmdprdsplit2lem  17207  dpjidcl  17220  dpjidclOLD  17227  ablfac1b  17234  ablfac1eu  17237  isdrng2  17519  drngmcl  17522  drngid2  17525  isdrngd  17534  xrs1mnd  18569  xrs10  18570  xrs1cmn  18571  xrge0subm  18572  xrge0cmn  18573  cnmsubglem  18593  expghm  18626  cnmsgngrp  18706  psgninv  18709  dsmmfi  18860  islinds2  18933  lindsind2  18939  lindfrn  18941  islindf4  18958  mdetdiaglem  19185  mdetrsca2  19191  mdetrlin2  19194  mdetralt  19195  mdetunilem5  19203  mdetunilem9  19207  maducoeval2  19227  smadiadetglem1  19258  isopn2  19618  ntrval2  19637  ntrdif  19638  clsdif  19639  ntrss  19641  cmclsopn  19648  cmntrcldOLD  19650  discld  19676  mretopd  19679  lpsscls  19728  restntr  19769  cmpcld  19988  2ndcsep  20045  1stccnp  20048  llycmpkgen2  20136  1stckgen  20140  txkgen  20238  qtopcld  20299  qtopcmap  20305  kqdisj  20318  isufil2  20494  ufileu  20505  filufint  20506  fixufil  20508  cfinufil  20514  ufilen  20516  fin1aufil  20518  supnfcls  20606  flimfnfcls  20614  alexsublem  20629  alexsubALTlem3  20634  cldsubg  20694  imasdsf1olem  20961  recld2  21404  sszcld  21407  xrge0gsumle  21423  divcn  21457  cdivcncf  21506  bcth3  21855  ismbl2  22023  cmmbl  22030  nulmbl  22031  nulmbl2  22032  unmbl  22033  voliunlem1  22045  voliunlem2  22046  ioombl1lem4  22056  ioombl1  22057  uniioombllem3  22079  mbfss  22138  itg1cl  22177  itg1ge0  22178  i1f0  22179  i1f1  22182  i1fmul  22188  itg1addlem4  22191  itg1mulc  22196  itg10a  22202  itg1ge0a  22203  itg1climres  22206  itg2cnlem1  22253  itgioo  22307  itgsplitioo  22329  limcdif  22365  ellimc2  22366  ellimc3  22368  limcflflem  22369  limcflf  22370  limcmo  22371  limcresi  22374  dvreslem  22398  dvres2lem  22399  dvidlem  22404  dvcnp2  22408  dvaddbr  22426  dvmulbr  22427  dvcobr  22434  dvrec  22443  dvcnvlem  22462  lhop1lem  22499  lhop  22502  tdeglem4  22543  deg1n0ima  22574  aacjcl  22808  taylthlem2  22854  abelth  22921  logcnlem5  23114  dvlog2  23121  efopnlem2  23125  cxpcn2  23207  sqrtcn  23211  efrlim  23416  jensen  23435  amgm  23437  wilthlem2  23460  dchrelbas2  23629  rpvmasum2  23814  dchrisum0re  23815  dchrisum0lem3  23821  dchrisum0  23822  tgisline  24127  umgrass  24440  frgrawopreg2  25172  xrge00  27827  qtophaus  27993  fsumcvg4  28086  gsumesum  28207  esum2dlem  28240  pwsiga  28279  sigainb  28285  carsggect  28445  omsmeas  28450  sitgclg  28467  ballotlemfelz  28612  ballotlemfp1  28613  ballotth  28659  lgamgulmlem2  28761  lgamucov  28769  kur14lem6  28844  kur14lem7  28845  cvmscld  28907  mclsppslem  29132  fundmpss  29362  wfi  29452  frind  29488  wfrlem16  29523  relsset  29691  limitssson  29714  fnsingle  29722  funimage  29731  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  voliunnfl  30223  cnambfre  30228  dvtan  30231  dvcncxp1  30266  dvcnsqrt  30267  dvasin  30269  dvacos  30270  areacirclem4  30276  cldbnd  30310  clsun  30312  fdc  30404  divrngcl  30526  isdrngo2  30527  isdrngo3  30528  istopclsd  30798  diophin  30871  setindtr  31132  dnnumch1  31156  cntzsdrg  31319  isdomn3  31332  deg1mhm  31335  sumnnodd  31802  cncficcgt0  31857  cncfiooicclem1  31862  cxpcncf2  31869  dirkercncflem2  32052  fourierdlem62  32117  fourierdlem66  32121  fourierdlem68  32123  fourierdlem95  32150  etransclem24  32207  etransclem44  32227  lindslinindimp2lem2  33260  islsati  35132  hdmap14lem2a  38010