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

Theorem snssd 3903
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 3892 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 202 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1721    C_ wss 3280   {csn 3774
This theorem is referenced by:  frirr  4519  fr3nr  4719  sofld  5277  oeeui  6804  ecinxp  6938  xpdom3  7165  domunsn  7216  mapdom3  7238  isinf  7281  ac6sfi  7310  pwfilem  7359  finsschain  7371  ssfii  7382  marypha1lem  7396  unxpwdom2  7512  mapfien  7609  fseqenlem1  7861  axdc3lem4  8289  axdc4lem  8291  ttukeylem7  8351  fpwwe2lem13  8473  canthwe  8482  canthp1lem1  8483  wuncval2  8578  un0addcl  10209  un0mulcl  10210  fseq1p1m1  11077  hashbclem  11656  hashf1lem1  11659  fsumge1  12531  incexclem  12571  isumltss  12583  rpnnen2lem11  12779  bitsinv1  12909  phicl2  13112  vdwlem1  13304  vdwlem8  13311  vdwlem12  13315  vdwlem13  13316  0ram  13343  ramub1lem1  13349  ramub1lem2  13350  ramcl  13352  imasaddfnlem  13708  imasaddflem  13710  imasvscafn  13717  imasvscaf  13719  mrieqvlemd  13809  mreexmrid  13823  mreexexlem4d  13827  acsfiindd  14558  acsmapd  14559  gsumvallem2  14727  gsumress  14732  0subg  14920  cycsubg2cl  14933  odf1o1  15161  gex1  15180  sylow2alem1  15206  sylow2alem2  15207  lsm01  15258  lsm02  15259  lsmdisj  15268  lsmdisj2  15269  prmcyg  15458  gsumzadd  15482  gsumconst  15487  gsumpt  15500  gsumxp  15505  dmdprdd  15515  dprdfadd  15533  dprdres  15541  dprdz  15543  dprdsn  15549  dprddisj2  15552  dprd2da  15555  dprd2d2  15557  dmdprdsplit2lem  15558  dpjcntz  15565  dpjdisj  15566  dpjlsm  15567  dpjidcl  15571  ablfacrp  15579  ablfac1eu  15586  pgpfac1lem1  15587  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem5  15592  pgpfaclem2  15595  lsssn0  15979  lss0ss  15980  lsptpcl  16010  lspsnvsi  16035  lspun0  16042  lsmpr  16116  lsppr  16120  lspsntri  16124  lspsolvlem  16169  lspsolv  16170  lsppratlem1  16174  lsppratlem3  16176  lsppratlem4  16177  islbs3  16182  lbsextlem4  16188  rsp1  16250  lidlnz  16254  lidldvgen  16281  psrlidm  16422  psrridm  16423  mplmonmul  16482  mulgrhm2  16743  zndvds  16785  en2top  17005  rest0  17187  ordtrest  17220  iscnp4  17281  cnconst2  17301  cnpdis  17311  ist1-2  17365  cnt1  17368  dishaus  17400  discmp  17415  cmpcld  17419  concompid  17447  dis2ndc  17476  dislly  17513  llycmpkgen2  17535  cmpkgen  17536  1stckgenlem  17538  1stckgen  17539  ptbasfi  17566  txdis  17617  txdis1cn  17620  txcmplem1  17626  xkohaus  17638  xkoptsub  17639  xkoinjcn  17672  pt1hmeo  17791  snfbas  17851  trnei  17877  isufil2  17893  ufileu  17904  filufint  17905  uffixsn  17910  ufildom1  17911  flimopn  17960  hausflim  17966  flimcf  17967  flimclslem  17969  flimsncls  17971  cnpflf2  17985  cnpflf  17986  fclsneii  18002  fclsfnflim  18012  fcfnei  18020  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  cldsubg  18093  snclseqg  18098  divstgphaus  18105  tsmsgsum  18121  tsmsid  18122  tgptsmscld  18133  tsmsxplem1  18135  tsmsxplem2  18136  ust0  18202  ustuqtop1  18224  neipcfilu  18279  prdsdsf  18350  prdsxmetlem  18351  prdsmet  18353  imasdsf1olem  18356  xpsdsval  18364  prdsbl  18474  prdsxmslem2  18512  idnghm  18730  icccmplem2  18807  metnrmlem2  18843  ioombl  19412  volivth  19452  itg11  19536  i1fmulclem  19547  itg2mulclem  19591  itgsplitioo  19682  limcvallem  19711  limcdif  19716  ellimc2  19717  limcflf  19721  limcmpt2  19724  limcres  19726  cnplimc  19727  limccnp  19731  limccnp2  19732  limcco  19733  dvreslem  19749  dvaddbr  19777  dvmulbr  19778  dvcmulf  19784  dvef  19817  dvivth  19847  lhop2  19852  lhop  19853  ply1remlem  20038  fta1blem  20044  ig1peu  20047  ig1pdvds  20052  plyco0  20064  elply2  20068  plyf  20070  elplyr  20073  elplyd  20074  ply1term  20076  ply0  20080  plyeq0lem  20082  plyeq0  20083  plypf1  20084  plyaddlem  20087  plymullem  20088  dgrlem  20101  coef2  20103  coeidlem  20109  plyco  20113  coemulhi  20125  plycj  20148  vieta1  20182  taylf  20230  radcnv0  20285  abelth  20310  rlimcnp  20757  xrlimcnp  20760  amgm  20782  wilthlem2  20805  basellem7  20822  basellem9  20824  ppiprm  20887  chtprm  20889  musumsum  20930  muinv  20931  logexprlim  20962  perfectlem2  20967  dchrhash  21008  rpvmasum2  21159  umgraex  21311  umgra1  21314  uslgra1  21345  usgra1  21346  uvtxnm1nbgra  21456  constr1trl  21541  eupa0  21649  eupap1  21651  0oo  22243  sh0le  22895  kerf1hrm  24215  esumsn  24409  subfacp1lem1  24818  subfacp1lem5  24823  erdszelem4  24833  erdszelem8  24837  sconpi1  24879  cvmscld  24913  cvmlift2lem6  24948  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  wfrlem15  25484  axlowdimlem7  25791  axlowdimlem10  25794  comppfsc  26277  neibastop2lem  26279  topjoin  26284  fnejoin2  26288  prdsbnd  26392  heiborlem8  26417  rrnequiv  26434  grpokerinj  26450  0idl  26525  prnc  26567  isfldidl  26568  ralxpmap  26632  elrfi  26638  cmpfiiin  26641  mzpcompact2lem  26698  dfac11  27028  pwssplit1  27056  pwssplit4  27059  rngunsnply  27246  flcidc  27247  en2other2  27250  pmtrprfv  27264  acsfn1p  27375  proot1mul  27383  bnj1452  29127  lshpnel2N  29468  lsatfixedN  29492  lfl0f  29552  lkrlsp3  29587  elpaddatriN  30285  elpaddat  30286  elpadd2at  30288  pmodlem1  30328  osumcllem1N  30438  osumcllem2N  30439  osumcllem9N  30446  osumcllem10N  30447  pexmidlem6N  30457  pexmidlem7N  30458  dibss  31652  dochocsn  31864  dochsncom  31865  dochnel  31876  dihprrnlem1N  31907  dihprrnlem2  31908  djhlsmat  31910  dihsmsprn  31913  dvh4dimlem  31926  dvhdimlem  31927  dochsnnz  31933  dochsatshp  31934  dochsnshp  31936  dochexmid  31951  dochsnkr  31955  dochsnkr2cl  31957  dochfl1  31959  lcfl7lem  31982  lcfl6  31983  lcfl8  31985  lcfl9a  31988  lclkrlem2a  31990  lclkrlem2c  31992  lclkrlem2d  31993  lclkrlem2e  31994  lclkrlem2j  31999  lclkrlem2o  32004  lclkrlem2p  32005  lclkrlem2s  32008  lclkrlem2v  32011  lcfrlem14  32039  lcfrlem18  32043  lcfrlem19  32044  lcfrlem20  32045  lcfrlem23  32048  lcfrlem25  32050  lcdlkreqN  32105  mapdval4N  32115  mapdsn  32124  mapdhvmap  32252  hdmaprnlem4tN  32338  hdmapinvlem1  32404  hdmapinvlem2  32405  hdmapinvlem3  32406  hdmapinvlem4  32407  hdmapglem5  32408  hgmapvvlem3  32411  hdmapglem7a  32413  hdmapglem7b  32414  hdmapglem7  32415  hdmapoc  32417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-sn 3780
  Copyright terms: Public domain W3C validator