MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difss Structured version   Unicode version

Theorem difss 3474
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.
StepHypRef Expression
1 eldifi 3469 . 2  |-  ( x  e.  ( A  \  B )  ->  x  e.  A )
21ssriv 3352 1  |-  ( A 
\  B )  C_  A
Colors of variables: wff set class
Syntax hints:    \ cdif 3317    C_ wss 3320
This theorem is referenced by:  difssd  3475  difss2  3476  ssdifss  3478  disj4  3676  0dif  3699  uneqdifeq  3716  difsnpss  3941  unidif  4047  iunxdif2  4139  difexg  4351  tz7.7  4607  tfi  4833  peano5  4868  reldif  4994  cnvdif  5278  fresaun  5614  fresaunres2  5615  resdif  5696  fndmdif  5834  difxp  6380  oev  6758  oelim2  6838  swoer  6933  swoord1  6934  swoord2  6935  boxcutc  7105  undom  7196  domunsncan  7208  sbthlem2  7218  sbthlem4  7220  sbthlem5  7221  limenpsi  7282  phplem2  7287  php  7291  php3  7293  pssnn  7327  diffi  7339  frfi  7352  fofinf1o  7387  ixpfi2  7405  elfiun  7435  marypha1lem  7438  wemapso  7520  inf3lem3  7585  infdifsn  7611  cantnflem2  7646  dfac8alem  7910  acnnum  7933  inffien  7944  kmlem5  8034  infdif  8089  infdif2  8090  ackbij1lem18  8117  fictb  8125  fin23lem7  8196  fin23lem11  8197  fin23lem28  8220  fin23lem30  8222  compsscnvlem  8250  isf34lem2  8253  compssiso  8254  isf34lem4  8257  fin1a2lem7  8286  domtriomlem  8322  axcclem  8337  zornn0g  8385  ttukey2g  8396  konigthlem  8443  pinn  8755  niex  8758  ltsopi  8765  dmaddpi  8767  dmmulpi  8768  lerelxr  9141  mulnzcnopr  9668  dflt2  10741  expcl2lem  11393  expclzlem  11405  hashun2  11657  fsumss  12519  fsumless  12575  cvgcmpce  12597  rpnnen2lem9  12822  isstruct2  13478  structcnvcnv  13480  strleun  13559  strle1  13560  mreexexlem2d  13870  frgpnabllem2  15485  dprdss  15587  dprd2da  15600  dmdprdsplit2lem  15603  dpjidcl  15616  ablfac1b  15628  ablfac1eu  15631  isdrng2  15845  drngmcl  15848  drngid2  15851  isdrngd  15860  xrs1mnd  16736  xrs10  16737  xrs1cmn  16738  xrge0subm  16739  xrge0cmn  16740  cnmsubglem  16761  expghm  16777  isopn2  17096  ntrval2  17115  ntrdif  17116  clsdif  17117  ntrss  17119  cmclsopn  17126  cmntrcld  17127  discld  17153  mretopd  17156  lpsscls  17205  islp3  17210  restntr  17246  cmpcld  17465  2ndcsep  17522  1stccnp  17525  llycmpkgen2  17582  1stckgen  17586  txkgen  17684  qtopcld  17745  qtopcmap  17751  kqdisj  17764  isufil2  17940  ufileu  17951  filufint  17952  fixufil  17954  cfinufil  17960  ufilen  17962  fin1aufil  17964  supnfcls  18052  flimfnfcls  18060  alexsublem  18075  alexsubALTlem3  18080  cldsubg  18140  imasdsf1olem  18403  recld2  18845  sszcld  18848  xrge0gsumle  18864  divcn  18898  cdivcncf  18947  bcth3  19284  ismbl2  19423  cmmbl  19429  nulmbl  19430  nulmbl2  19431  unmbl  19432  voliunlem1  19444  voliunlem2  19445  ioombl1lem4  19455  ioombl1  19456  uniioombllem3  19477  mbfss  19538  itg1cl  19577  itg1ge0  19578  i1f0  19579  i1f1  19582  i1fmul  19588  itg1addlem4  19591  itg1mulc  19596  itg10a  19602  itg1ge0a  19603  itg1climres  19606  itg2cnlem1  19653  itgioo  19707  itgsplitioo  19729  limcdif  19763  ellimc2  19764  ellimc3  19766  limcflflem  19767  limcflf  19768  limcmo  19769  limcresi  19772  dvreslem  19796  dvres2lem  19797  dvidlem  19802  dvcnp2  19806  dvaddbr  19824  dvmulbr  19825  dvcobr  19832  dvrec  19841  dvcnvlem  19860  lhop1lem  19897  lhop  19900  tdeglem4  19983  deg1n0ima  20012  aacjcl  20244  taylthlem2  20290  abelth  20357  logcnlem5  20537  dvlog2  20544  efopnlem2  20548  cxpcn2  20630  sqrcn  20634  efrlim  20808  jensen  20827  amgm  20829  wilthlem2  20852  dchrelbas2  21021  rpvmasum2  21206  dchrisum0re  21207  dchrisum0lem3  21213  dchrisum0  21214  umgrass  21354  xrge00  24208  gsumpropd2lem  24220  gsumesum  24451  pwsiga  24513  sigainb  24519  sibfof  24654  sitgclg  24656  ballotlemfelz  24748  ballotlemfp1  24749  ballotth  24795  lgamgulmlem2  24814  lgamucov  24822  kur14lem6  24897  kur14lem7  24898  cvmscld  24960  fprodss  25274  fundmpss  25390  wfi  25482  frind  25518  wfrlem16  25553  relsset  25733  limitssson  25756  fnsingle  25764  funimage  25773  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  voliunnfl  26250  cnambfre  26255  areacirclem4  26295  cldbnd  26329  clsun  26331  fdc  26449  divrngcl  26573  isdrngo2  26574  isdrngo3  26575  ralxpmap  26742  istopclsd  26754  diophin  26831  setindtr  27095  dnnumch1  27119  dsmmfi  27181  islinds2  27260  lindsind2  27266  lindfrn  27268  islindf4  27285  f1omvdmvd  27363  mvdco  27365  f1omvdconj  27366  pmtrfb  27383  pmtrfconj  27384  symggen  27388  symggen2  27389  psgnunilem1  27393  cnmsgngrp  27413  psgnghm2  27415  cntzsdrg  27487  isdomn3  27500  deg1mhm  27503  frgrawopreg2  28440  islsati  29792  hdmap14lem2a  32668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator