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

Theorem snssd 4006
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 3995 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 210 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1755    C_ wss 3316   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-in 3323  df-ss 3330  df-sn 3866
This theorem is referenced by:  frirr  4684  sofld  5274  fr3nr  6380  oeeui  7029  ecinxp  7163  ralxpmap  7250  xpdom3  7397  domunsn  7449  mapdom3  7471  isinf  7514  ac6sfi  7544  pwfilem  7593  finsschain  7606  ssfii  7657  marypha1lem  7671  unxpwdom2  7791  mapfienOLD  7915  en2other2  8164  fseqenlem1  8182  axdc3lem4  8610  axdc4lem  8612  ttukeylem7  8672  fpwwe2lem13  8797  canthwe  8806  canthp1lem1  8807  wuncval2  8902  un0addcl  10601  un0mulcl  10602  fseq1p1m1  11518  hashbclem  12189  hashf1lem1  12192  fsumge1  13243  incexclem  13282  isumltss  13294  rpnnen2lem11  13490  bitsinv1  13621  phicl2  13826  vdwlem1  14025  vdwlem8  14032  vdwlem12  14036  vdwlem13  14037  0ram  14064  ramub1lem1  14070  ramub1lem2  14071  ramcl  14073  imasaddfnlem  14449  imasaddflem  14451  imasvscafn  14458  imasvscaf  14460  mrieqvlemd  14550  mreexmrid  14564  mreexexlem4d  14568  acsfiindd  15330  acsmapd  15331  gsumvallem2  15483  gsumress  15487  0subg  15686  cycsubg2cl  15699  pmtrprfv  15939  odf1o1  16051  gex1  16070  sylow2alem1  16096  sylow2alem2  16097  lsm01  16148  lsm02  16149  lsmdisj  16158  lsmdisj2  16159  prmcyg  16350  gsumzadd  16389  gsumzaddOLD  16391  gsumconst  16406  gsumpt  16429  gsumptOLD  16430  gsumxp  16442  gsumxpOLD  16444  dmdprdd  16455  dprdfadd  16484  dprdfaddOLD  16491  dprdres  16499  dprdz  16501  dprdsn  16507  dprddisj2  16511  dprddisj2OLD  16512  dprd2da  16515  dprd2d2  16517  dmdprdsplit2lem  16518  dpjcntz  16525  dpjdisj  16526  dpjlsm  16527  dpjidcl  16531  dpjidclOLD  16538  ablfacrp  16541  ablfac1eu  16548  pgpfac1lem1  16549  pgpfac1lem3a  16551  pgpfac1lem3  16552  pgpfac1lem5  16554  pgpfaclem2  16557  lsssn0  16951  lss0ss  16952  lsptpcl  16982  lspsnvsi  17007  lspun0  17014  pwssplit1  17062  lsmpr  17092  lsppr  17096  lspsntri  17100  lspsolvlem  17145  lspsolv  17146  lsppratlem1  17150  lsppratlem3  17152  lsppratlem4  17153  islbs3  17158  lbsextlem4  17164  rsp1  17228  lidlnz  17232  lidldvgen  17259  psrlidm  17408  psrlidmOLD  17409  psrridm  17410  psrridmOLD  17411  mplmonmul  17477  mulgrhm2  17769  mulgrhm2OLD  17772  zndvds  17824  mdet1  18250  mdetrlin  18251  mdetrsca  18252  mdetrsca2  18253  mdetrlin2  18255  mdetunilem5  18264  mdetunilem9  18268  mdetmul  18271  en2top  18432  rest0  18615  ordtrest  18648  iscnp4  18709  cnconst2  18729  cnpdis  18739  ist1-2  18793  cnt1  18796  dishaus  18828  discmp  18843  cmpcld  18847  concompid  18877  dis2ndc  18906  dislly  18943  llycmpkgen2  18965  cmpkgen  18966  1stckgenlem  18968  1stckgen  18969  ptbasfi  18996  txdis  19047  txdis1cn  19050  txcmplem1  19056  xkohaus  19068  xkoptsub  19069  xkoinjcn  19102  pt1hmeo  19221  snfbas  19281  trnei  19307  isufil2  19323  ufileu  19334  filufint  19335  uffixsn  19340  ufildom1  19341  flimopn  19390  hausflim  19396  flimcf  19397  flimclslem  19399  flimsncls  19401  cnpflf2  19415  cnpflf  19416  fclsneii  19432  fclsfnflim  19442  fcfnei  19450  alexsubALTlem3  19463  alexsubALTlem4  19464  ptcmplem2  19467  cldsubg  19523  snclseqg  19528  divstgphaus  19535  tsmsgsum  19551  tsmsid  19552  tsmsgsumOLD  19554  tsmsidOLD  19555  tgptsmscld  19567  tsmsxplem1  19569  tsmsxplem2  19570  ust0  19636  ustuqtop1  19658  neipcfilu  19713  prdsdsf  19784  prdsxmetlem  19785  prdsmet  19787  imasdsf1olem  19790  xpsdsval  19798  prdsbl  19908  prdsxmslem2  19946  idnghm  20164  icccmplem2  20242  metnrmlem2  20278  ioombl  20888  volivth  20929  itg11  21011  i1fmulclem  21022  itg2mulclem  21066  itgsplitioo  21157  limcvallem  21188  limcdif  21193  ellimc2  21194  limcflf  21198  limcmpt2  21201  limcres  21203  cnplimc  21204  limccnp  21208  limccnp2  21209  limcco  21210  dvreslem  21226  dvaddbr  21254  dvmulbr  21255  dvcmulf  21261  dvef  21294  dvivth  21324  lhop2  21329  lhop  21330  ply1remlem  21519  fta1blem  21525  ig1peu  21528  ig1pdvds  21533  plyco0  21545  elply2  21549  plyf  21551  elplyr  21554  elplyd  21555  ply1term  21557  ply0  21561  plyeq0lem  21563  plyeq0  21564  plypf1  21565  plyaddlem  21568  plymullem  21569  dgrlem  21582  coef2  21584  coeidlem  21590  plyco  21594  coemulhi  21606  plycj  21629  vieta1  21663  taylf  21711  radcnv0  21766  abelth  21791  rlimcnp  22244  xrlimcnp  22247  amgm  22269  wilthlem2  22292  basellem7  22309  basellem9  22311  ppiprm  22374  chtprm  22376  musumsum  22417  muinv  22418  logexprlim  22449  perfectlem2  22454  dchrhash  22495  rpvmasum2  22646  axlowdimlem7  23017  axlowdimlem10  23020  umgraex  23080  umgra1  23083  uslgra1  23114  usgra1  23115  uvtxnm1nbgra  23225  constr1trl  23310  eupa0  23418  eupap1  23420  0oo  24012  sh0le  24666  kerf1hrm  26145  ordtrestNEW  26205  esumsn  26369  eulerpartlems  26591  eulerpartlemgc  26593  eulerpartlemgh  26609  eulerpartlemgs2  26611  subfacp1lem1  26915  subfacp1lem5  26920  erdszelem4  26930  erdszelem8  26934  sconpi1  26976  cvmscld  27010  cvmlift2lem6  27045  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift2lem12  27051  wfrlem15  27585  comppfsc  28423  neibastop2lem  28425  topjoin  28430  fnejoin2  28434  prdsbnd  28536  heiborlem8  28561  rrnequiv  28578  grpokerinj  28594  0idl  28669  prnc  28711  isfldidl  28712  elrfi  28875  cmpfiiin  28878  mzpcompact2lem  28933  dfac11  29260  pwssplit4  29287  rngunsnply  29375  flcidc  29376  acsfn1p  29401  proot1mul  29409  iocinico  29432  fsumsplitsndif  30084  gsumdifsnd  30597  mdetdiaglem  30665  bnj1452  31766  lshpnel2N  32224  lsatfixedN  32248  lfl0f  32308  lkrlsp3  32343  elpaddatriN  33041  elpaddat  33042  elpadd2at  33044  pmodlem1  33084  osumcllem1N  33194  osumcllem2N  33195  osumcllem9N  33202  osumcllem10N  33203  pexmidlem6N  33213  pexmidlem7N  33214  dibss  34408  dochocsn  34620  dochsncom  34621  dochnel  34632  dihprrnlem1N  34663  dihprrnlem2  34664  djhlsmat  34666  dihsmsprn  34669  dvh4dimlem  34682  dvhdimlem  34683  dochsnnz  34689  dochsatshp  34690  dochsnshp  34692  dochexmid  34707  dochsnkr  34711  dochsnkr2cl  34713  dochfl1  34715  lcfl7lem  34738  lcfl6  34739  lcfl8  34741  lcfl9a  34744  lclkrlem2a  34746  lclkrlem2c  34748  lclkrlem2d  34749  lclkrlem2e  34750  lclkrlem2j  34755  lclkrlem2o  34760  lclkrlem2p  34761  lclkrlem2s  34764  lclkrlem2v  34767  lcfrlem14  34795  lcfrlem18  34799  lcfrlem19  34800  lcfrlem20  34801  lcfrlem23  34804  lcfrlem25  34806  lcdlkreqN  34861  mapdval4N  34871  mapdsn  34880  mapdhvmap  35008  hdmaprnlem4tN  35094  hdmapinvlem1  35160  hdmapinvlem2  35161  hdmapinvlem3  35162  hdmapinvlem4  35163  hdmapglem5  35164  hgmapvvlem3  35167  hdmapglem7a  35169  hdmapglem7b  35170  hdmapglem7  35171  hdmapoc  35173
  Copyright terms: Public domain W3C validator