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

Theorem snssd 4083
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 4071 . . 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 1872    C_ wss 3374   {csn 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-v 3019  df-in 3381  df-ss 3388  df-sn 3937
This theorem is referenced by:  frirr  4768  sofld  5241  fsnex  6135  fr3nr  6559  wfrlem15  7000  oeeui  7253  ecinxp  7388  ralxpmap  7471  xpdom3  7618  domunsn  7670  mapdom3  7692  isinf  7733  ac6sfi  7763  pwfilem  7816  finsschain  7829  ssfii  7881  marypha1lem  7895  unxpwdom2  8051  en2other2  8387  fseqenlem1  8401  axdc3lem4  8829  axdc4lem  8831  ttukeylem7  8891  fpwwe2lem13  9013  canthwe  9022  canthp1lem1  9023  wuncval2  9118  un0addcl  10849  un0mulcl  10850  fseq1p1m1  11814  hashbclem  12558  hashf1lem1  12561  fsumge1  13795  incexclem  13832  isumltss  13844  rpnnen2lem11  14215  bitsinv1  14354  lcmfunsnlem2  14551  lcmfass  14557  phicl2  14654  vdwlem1  14869  vdwlem8  14876  vdwlem12  14880  vdwlem13  14881  0ram  14916  ramub1lem1  14922  ramub1lem2  14923  ramcl  14925  imasaddfnlem  15372  imasaddflem  15374  imasvscafn  15381  imasvscaf  15383  mrieqvlemd  15473  mreexmrid  15487  mreexexlem4d  15491  acsfiindd  16361  acsmapd  16362  gsumress  16457  gsumvallem2  16557  0subg  16780  cycsubg2cl  16793  pmtrprfv  17032  odf1o1  17159  gex1  17181  sylow2alem1  17207  sylow2alem2  17208  lsm01  17259  lsm02  17260  lsmdisj  17269  lsmdisj2  17270  prmcyg  17466  gsumzadd  17493  gsumconst  17505  gsumdifsnd  17531  gsumpt  17532  gsumxp  17546  dmdprdd  17569  dprdfadd  17591  dprdres  17599  dprdz  17601  dprdsn  17607  dprddisj2  17610  dprd2da  17613  dprd2d2  17615  dmdprdsplit2lem  17616  dpjcntz  17623  dpjdisj  17624  dpjlsm  17625  dpjidcl  17629  ablfacrp  17637  ablfac1eu  17644  pgpfac1lem1  17645  pgpfac1lem3a  17647  pgpfac1lem3  17648  pgpfac1lem5  17650  pgpfaclem2  17653  kerf1hrm  17909  lsssn0  18109  lss0ss  18110  lsptpcl  18140  lspsnvsi  18165  lspun0  18172  pwssplit1  18220  lsmpr  18250  lsppr  18254  lspsntri  18258  lspsolvlem  18303  lspsolv  18304  lsppratlem1  18308  lsppratlem3  18310  lsppratlem4  18311  islbs3  18316  lbsextlem4  18322  rsp1  18386  lidlnz  18390  lidldvgen  18417  psrlidm  18565  psrridm  18566  mplmonmul  18626  mulgrhm2  19007  zndvds  19057  mdetdiaglem  19560  mdetrlin  19564  mdetrsca  19565  mdetrsca2  19566  mdetrlin2  19569  mdetunilem5  19578  mdetunilem9  19582  mdetmul  19585  en2top  19938  rest0  20122  ordtrest  20155  iscnp4  20216  cnconst2  20236  cnpdis  20246  ist1-2  20300  cnt1  20303  dishaus  20335  discmp  20350  cmpcld  20354  concompid  20383  dis2ndc  20412  dislly  20449  dissnref  20480  comppfsc  20484  llycmpkgen2  20502  cmpkgen  20503  1stckgenlem  20505  1stckgen  20506  ptbasfi  20533  txdis  20584  txdis1cn  20587  txcmplem1  20593  xkohaus  20605  xkoptsub  20606  xkoinjcn  20639  pt1hmeo  20758  snfbas  20818  trnei  20844  isufil2  20860  ufileu  20871  filufint  20872  uffixsn  20877  ufildom1  20878  flimopn  20927  hausflim  20933  flimcf  20934  flimclslem  20936  flimsncls  20938  cnpflf2  20952  cnpflf  20953  fclsneii  20969  fclsfnflim  20979  fcfnei  20987  flfcntr  20995  alexsubALTlem3  21001  alexsubALTlem4  21002  ptcmplem2  21005  cldsubg  21062  snclseqg  21067  qustgphaus  21074  tsmsgsum  21090  tsmsid  21091  tgptsmscld  21102  tsmsxplem1  21104  tsmsxplem2  21105  ust0  21171  ustuqtop1  21193  neipcfilu  21248  prdsdsf  21319  prdsxmetlem  21320  prdsmet  21322  imasdsf1olem  21325  xpsdsval  21333  prdsbl  21443  prdsxmslem2  21481  idnghm  21701  icccmplem2  21778  metnrmlem2  21814  metnrmlem2OLD  21829  ioombl  22455  volivth  22502  itg11  22586  i1fmulclem  22597  itg2mulclem  22641  itgsplitioo  22732  limcvallem  22763  limcdif  22768  ellimc2  22769  limcflf  22773  limcmpt2  22776  limcres  22778  cnplimc  22779  limccnp  22783  limccnp2  22784  limcco  22785  dvreslem  22801  dvaddbr  22829  dvmulbr  22830  dvcmulf  22836  dvef  22869  dvivth  22899  lhop2  22904  lhop  22905  ply1remlem  23050  fta1blem  23056  ig1peu  23059  ig1peuOLD  23060  ig1pdvds  23065  ig1pdvdsOLD  23071  plyco0  23083  elply2  23087  plyf  23089  elplyr  23092  elplyd  23093  ply1term  23095  ply0  23099  plyeq0lem  23101  plyeq0  23102  plypf1  23103  plyaddlem  23106  plymullem  23107  dgrlem  23120  coef2  23122  coeidlem  23128  plyco  23132  coemulhi  23145  plycj  23168  vieta1  23202  taylf  23253  radcnv0  23308  abelth  23333  rlimcnp  23828  xrlimcnp  23831  amgm  23853  wilthlem2  23931  basellem7  23950  basellem9  23952  ppiprm  24015  chtprm  24017  musumsum  24058  muinv  24059  logexprlim  24090  perfectlem2  24095  dchrhash  24136  rpvmasum2  24287  axlowdimlem7  24915  axlowdimlem10  24918  umgraex  24987  umgra1  24990  uslgra1  25036  usgra1  25037  uvtxnm1nbgra  25159  constr1trl  25255  eupa0  25639  eupap1  25641  0oo  26367  sh0le  27030  disjiunel  28147  qtopt1  28609  locfinref  28615  ordtrestNEW  28674  esumsnf  28832  rossros  28949  oms0  29072  carsggect  29097  eulerpartlems  29140  eulerpartlemgc  29142  eulerpartlemgh  29158  eulerpartlemgs2  29160  plymulx0  29383  bnj1452  29808  subfacp1lem1  29849  subfacp1lem5  29854  erdszelem4  29864  erdszelem8  29868  sconpi1  29909  cvmscld  29943  cvmlift2lem6  29978  cvmlift2lem9  29981  cvmlift2lem11  29983  cvmlift2lem12  29984  mrsubvrs  30107  neibastop2lem  30960  topjoin  30965  fnejoin2  30969  poimirlem3  31850  poimirlem9  31856  poimirlem28  31875  poimirlem32  31879  prdsbnd  32032  heiborlem8  32057  rrnequiv  32074  grpokerinj  32090  0idl  32165  prnc  32207  isfldidl  32208  lshpnel2N  32463  lsatfixedN  32487  lfl0f  32547  lkrlsp3  32582  elpaddatriN  33280  elpaddat  33281  elpadd2at  33283  pmodlem1  33323  osumcllem1N  33433  osumcllem2N  33434  osumcllem9N  33441  osumcllem10N  33442  pexmidlem6N  33452  pexmidlem7N  33453  dibss  34649  dochocsn  34861  dochsncom  34862  dochnel  34873  dihprrnlem1N  34904  dihprrnlem2  34905  djhlsmat  34907  dihsmsprn  34910  dvh4dimlem  34923  dvhdimlem  34924  dochsnnz  34930  dochsatshp  34931  dochsnshp  34933  dochexmid  34948  dochsnkr  34952  dochsnkr2cl  34954  dochfl1  34956  lcfl7lem  34979  lcfl6  34980  lcfl8  34982  lcfl9a  34985  lclkrlem2a  34987  lclkrlem2c  34989  lclkrlem2d  34990  lclkrlem2e  34991  lclkrlem2j  34996  lclkrlem2o  35001  lclkrlem2p  35002  lclkrlem2s  35005  lclkrlem2v  35008  lcfrlem14  35036  lcfrlem18  35040  lcfrlem19  35041  lcfrlem20  35042  lcfrlem23  35045  lcfrlem25  35047  lcdlkreqN  35102  mapdval4N  35112  mapdsn  35121  mapdhvmap  35249  hdmaprnlem4tN  35335  hdmapinvlem1  35401  hdmapinvlem2  35402  hdmapinvlem3  35403  hdmapinvlem4  35404  hdmapglem5  35405  hgmapvvlem3  35408  hdmapglem7a  35410  hdmapglem7b  35411  hdmapglem7  35412  hdmapoc  35414  elrfi  35448  cmpfiiin  35451  mzpcompact2lem  35505  dfac11  35833  pwssplit4  35860  rngunsnply  35952  flcidc  35953  acsfn1p  35978  proot1mul  35986  iocinico  36009  iunrelexp0  36207  frege81d  36252  binomcxplemnn0  36611  fsumsplit1  37535  islptre  37582  limciccioolb  37584  limcicciooub  37600  limcresiooub  37606  limcresioolb  37607  ioccncflimc  37646  icccncfext  37648  icocncflimc  37650  cncfiooicc  37655  dvnprodlem2  37705  dirkercncflem2  37849  dirkercncflem3  37850  fourierdlem48  37901  fourierdlem49  37902  fourierdlem79  37932  fourierdlem101  37954  sge0sup  38084  hoidmvlelem2  38265  perfectALTVlem2  38657  fsumsplitsndif  38866  upgrex  38958  upgr1elem  38970  uvtxanm1nbgr  39207  gsumdifsndf  39740
  Copyright terms: Public domain W3C validator