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

Theorem snssd 4148
Description: The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
snssd.1  |-  ( ph  ->  A  e.  B )
Assertion
Ref Expression
snssd  |-  ( ph  ->  { A }  C_  B )

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2  |-  ( ph  ->  A  e.  B )
2 snssg 4136 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 213 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    e. wcel 1870    C_ wss 3442   {csn 4002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3089  df-in 3449  df-ss 3456  df-sn 4003
This theorem is referenced by:  frirr  4831  sofld  5304  fsnex  6196  fr3nr  6620  wfrlem15  7058  oeeui  7311  ecinxp  7446  ralxpmap  7529  xpdom3  7676  domunsn  7728  mapdom3  7750  isinf  7791  ac6sfi  7821  pwfilem  7874  finsschain  7887  ssfii  7939  marypha1lem  7953  unxpwdom2  8103  en2other2  8439  fseqenlem1  8453  axdc3lem4  8881  axdc4lem  8883  ttukeylem7  8943  fpwwe2lem13  9066  canthwe  9075  canthp1lem1  9076  wuncval2  9171  un0addcl  10903  un0mulcl  10904  fseq1p1m1  11866  hashbclem  12610  hashf1lem1  12613  fsumge1  13835  incexclem  13872  isumltss  13884  rpnnen2lem11  14255  bitsinv1  14390  lcmfunsnlem2  14575  lcmfass  14581  phicl2  14676  vdwlem1  14885  vdwlem8  14892  vdwlem12  14896  vdwlem13  14897  0ram  14932  ramub1lem1  14938  ramub1lem2  14939  ramcl  14941  imasaddfnlem  15376  imasaddflem  15378  imasvscafn  15385  imasvscaf  15387  mrieqvlemd  15477  mreexmrid  15491  mreexexlem4d  15495  acsfiindd  16365  acsmapd  16366  gsumress  16461  gsumvallem2  16561  0subg  16784  cycsubg2cl  16797  pmtrprfv  17036  odf1o1  17150  gex1  17169  sylow2alem1  17195  sylow2alem2  17196  lsm01  17247  lsm02  17248  lsmdisj  17257  lsmdisj2  17258  prmcyg  17454  gsumzadd  17481  gsumconst  17493  gsumdifsnd  17519  gsumpt  17520  gsumxp  17534  dmdprdd  17557  dprdfadd  17579  dprdres  17587  dprdz  17589  dprdsn  17595  dprddisj2  17598  dprd2da  17601  dprd2d2  17603  dmdprdsplit2lem  17604  dpjcntz  17611  dpjdisj  17612  dpjlsm  17613  dpjidcl  17617  ablfacrp  17625  ablfac1eu  17632  pgpfac1lem1  17633  pgpfac1lem3a  17635  pgpfac1lem3  17636  pgpfac1lem5  17638  pgpfaclem2  17641  kerf1hrm  17897  lsssn0  18097  lss0ss  18098  lsptpcl  18128  lspsnvsi  18153  lspun0  18160  pwssplit1  18208  lsmpr  18238  lsppr  18242  lspsntri  18246  lspsolvlem  18291  lspsolv  18292  lsppratlem1  18296  lsppratlem3  18298  lsppratlem4  18299  islbs3  18304  lbsextlem4  18310  rsp1  18374  lidlnz  18378  lidldvgen  18405  psrlidm  18553  psrridm  18554  mplmonmul  18614  mulgrhm2  18992  zndvds  19042  mdetdiaglem  19545  mdetrlin  19549  mdetrsca  19550  mdetrsca2  19551  mdetrlin2  19554  mdetunilem5  19563  mdetunilem9  19567  mdetmul  19570  en2top  19923  rest0  20107  ordtrest  20140  iscnp4  20201  cnconst2  20221  cnpdis  20231  ist1-2  20285  cnt1  20288  dishaus  20320  discmp  20335  cmpcld  20339  concompid  20368  dis2ndc  20397  dislly  20434  dissnref  20465  comppfsc  20469  llycmpkgen2  20487  cmpkgen  20488  1stckgenlem  20490  1stckgen  20491  ptbasfi  20518  txdis  20569  txdis1cn  20572  txcmplem1  20578  xkohaus  20590  xkoptsub  20591  xkoinjcn  20624  pt1hmeo  20743  snfbas  20803  trnei  20829  isufil2  20845  ufileu  20856  filufint  20857  uffixsn  20862  ufildom1  20863  flimopn  20912  hausflim  20918  flimcf  20919  flimclslem  20921  flimsncls  20923  cnpflf2  20937  cnpflf  20938  fclsneii  20954  fclsfnflim  20964  fcfnei  20972  flfcntr  20980  alexsubALTlem3  20986  alexsubALTlem4  20987  ptcmplem2  20990  cldsubg  21047  snclseqg  21052  qustgphaus  21059  tsmsgsum  21075  tsmsid  21076  tgptsmscld  21087  tsmsxplem1  21089  tsmsxplem2  21090  ust0  21156  ustuqtop1  21178  neipcfilu  21233  prdsdsf  21304  prdsxmetlem  21305  prdsmet  21307  imasdsf1olem  21310  xpsdsval  21318  prdsbl  21428  prdsxmslem2  21466  idnghm  21666  icccmplem2  21743  metnrmlem2  21779  ioombl  22386  volivth  22433  itg11  22517  i1fmulclem  22528  itg2mulclem  22572  itgsplitioo  22663  limcvallem  22694  limcdif  22699  ellimc2  22700  limcflf  22704  limcmpt2  22707  limcres  22709  cnplimc  22710  limccnp  22714  limccnp2  22715  limcco  22716  dvreslem  22732  dvaddbr  22760  dvmulbr  22761  dvcmulf  22767  dvef  22800  dvivth  22830  lhop2  22835  lhop  22836  ply1remlem  22979  fta1blem  22985  ig1peu  22988  ig1pdvds  22993  plyco0  23005  elply2  23009  plyf  23011  elplyr  23014  elplyd  23015  ply1term  23017  ply0  23021  plyeq0lem  23023  plyeq0  23024  plypf1  23025  plyaddlem  23028  plymullem  23029  dgrlem  23042  coef2  23044  coeidlem  23050  plyco  23054  coemulhi  23067  plycj  23090  vieta1  23124  taylf  23172  radcnv0  23227  abelth  23252  rlimcnp  23747  xrlimcnp  23750  amgm  23772  wilthlem2  23850  basellem7  23867  basellem9  23869  ppiprm  23932  chtprm  23934  musumsum  23975  muinv  23976  logexprlim  24007  perfectlem2  24012  dchrhash  24053  rpvmasum2  24204  axlowdimlem7  24815  axlowdimlem10  24818  umgraex  24887  umgra1  24890  uslgra1  24936  usgra1  24937  uvtxnm1nbgra  25058  constr1trl  25154  eupa0  25538  eupap1  25540  0oo  26266  sh0le  26919  disjiunel  28036  qtopt1  28492  locfinref  28498  ordtrestNEW  28557  esumsnf  28715  rossros  28832  carsggect  28970  eulerpartlems  29010  eulerpartlemgc  29012  eulerpartlemgh  29028  eulerpartlemgs2  29030  plymulx0  29215  bnj1452  29640  subfacp1lem1  29681  subfacp1lem5  29686  erdszelem4  29696  erdszelem8  29700  sconpi1  29741  cvmscld  29775  cvmlift2lem6  29810  cvmlift2lem9  29813  cvmlift2lem11  29815  cvmlift2lem12  29816  mrsubvrs  29939  neibastop2lem  30792  topjoin  30797  fnejoin2  30801  poimirlem3  31637  poimirlem9  31643  poimirlem28  31662  poimirlem32  31666  prdsbnd  31819  heiborlem8  31844  rrnequiv  31861  grpokerinj  31877  0idl  31952  prnc  31994  isfldidl  31995  lshpnel2N  32250  lsatfixedN  32274  lfl0f  32334  lkrlsp3  32369  elpaddatriN  33067  elpaddat  33068  elpadd2at  33070  pmodlem1  33110  osumcllem1N  33220  osumcllem2N  33221  osumcllem9N  33228  osumcllem10N  33229  pexmidlem6N  33239  pexmidlem7N  33240  dibss  34436  dochocsn  34648  dochsncom  34649  dochnel  34660  dihprrnlem1N  34691  dihprrnlem2  34692  djhlsmat  34694  dihsmsprn  34697  dvh4dimlem  34710  dvhdimlem  34711  dochsnnz  34717  dochsatshp  34718  dochsnshp  34720  dochexmid  34735  dochsnkr  34739  dochsnkr2cl  34741  dochfl1  34743  lcfl7lem  34766  lcfl6  34767  lcfl8  34769  lcfl9a  34772  lclkrlem2a  34774  lclkrlem2c  34776  lclkrlem2d  34777  lclkrlem2e  34778  lclkrlem2j  34783  lclkrlem2o  34788  lclkrlem2p  34789  lclkrlem2s  34792  lclkrlem2v  34795  lcfrlem14  34823  lcfrlem18  34827  lcfrlem19  34828  lcfrlem20  34829  lcfrlem23  34832  lcfrlem25  34834  lcdlkreqN  34889  mapdval4N  34899  mapdsn  34908  mapdhvmap  35036  hdmaprnlem4tN  35122  hdmapinvlem1  35188  hdmapinvlem2  35189  hdmapinvlem3  35190  hdmapinvlem4  35191  hdmapglem5  35192  hgmapvvlem3  35195  hdmapglem7a  35197  hdmapglem7b  35198  hdmapglem7  35199  hdmapoc  35201  elrfi  35235  cmpfiiin  35238  mzpcompact2lem  35292  dfac11  35616  pwssplit4  35643  rngunsnply  35728  flcidc  35729  acsfn1p  35754  proot1mul  35762  iocinico  35785  iunrelexp0  35923  frege81d  35968  binomcxplemnn0  36325  fsumsplit1  37216  islptre  37261  limciccioolb  37263  limcicciooub  37279  limcresiooub  37285  limcresioolb  37286  ioccncflimc  37325  icccncfext  37327  icocncflimc  37329  cncfiooicc  37334  dvnprodlem2  37381  dirkercncflem2  37525  dirkercncflem3  37526  fourierdlem48  37576  fourierdlem49  37577  fourierdlem79  37607  fourierdlem101  37629  sge0sup  37757  perfectALTVlem2  38224  fsumsplitsndif  38406  gsumdifsndf  38897
  Copyright terms: Public domain W3C validator