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

Theorem snssd 3907
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 3896 . . 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 3284   {csn 3778
This theorem is referenced by:  frirr  4523  fr3nr  4723  sofld  5281  oeeui  6808  ecinxp  6942  xpdom3  7169  domunsn  7220  mapdom3  7242  isinf  7285  ac6sfi  7314  pwfilem  7363  finsschain  7375  ssfii  7386  marypha1lem  7400  unxpwdom2  7516  mapfien  7613  fseqenlem1  7865  axdc3lem4  8293  axdc4lem  8295  ttukeylem7  8355  fpwwe2lem13  8477  canthwe  8486  canthp1lem1  8487  wuncval2  8582  un0addcl  10213  un0mulcl  10214  fseq1p1m1  11081  hashbclem  11660  hashf1lem1  11663  fsumge1  12535  incexclem  12575  isumltss  12587  rpnnen2lem11  12783  bitsinv1  12913  phicl2  13116  vdwlem1  13308  vdwlem8  13315  vdwlem12  13319  vdwlem13  13320  0ram  13347  ramub1lem1  13353  ramub1lem2  13354  ramcl  13356  imasaddfnlem  13712  imasaddflem  13714  imasvscafn  13721  imasvscaf  13723  mrieqvlemd  13813  mreexmrid  13827  mreexexlem4d  13831  acsfiindd  14562  acsmapd  14563  gsumvallem2  14731  gsumress  14736  0subg  14924  cycsubg2cl  14937  odf1o1  15165  gex1  15184  sylow2alem1  15210  sylow2alem2  15211  lsm01  15262  lsm02  15263  lsmdisj  15272  lsmdisj2  15273  prmcyg  15462  gsumzadd  15486  gsumconst  15491  gsumpt  15504  gsumxp  15509  dmdprdd  15519  dprdfadd  15537  dprdres  15545  dprdz  15547  dprdsn  15553  dprddisj2  15556  dprd2da  15559  dprd2d2  15561  dmdprdsplit2lem  15562  dpjcntz  15569  dpjdisj  15570  dpjlsm  15571  dpjidcl  15575  ablfacrp  15583  ablfac1eu  15590  pgpfac1lem1  15591  pgpfac1lem3a  15593  pgpfac1lem3  15594  pgpfac1lem5  15596  pgpfaclem2  15599  lsssn0  15983  lss0ss  15984  lsptpcl  16014  lspsnvsi  16039  lspun0  16046  lsmpr  16120  lsppr  16124  lspsntri  16128  lspsolvlem  16173  lspsolv  16174  lsppratlem1  16178  lsppratlem3  16180  lsppratlem4  16181  islbs3  16186  lbsextlem4  16192  rsp1  16254  lidlnz  16258  lidldvgen  16285  psrlidm  16426  psrridm  16427  mplmonmul  16486  mulgrhm2  16747  zndvds  16789  en2top  17009  rest0  17191  ordtrest  17224  iscnp4  17285  cnconst2  17305  cnpdis  17315  ist1-2  17369  cnt1  17372  dishaus  17404  discmp  17419  cmpcld  17423  concompid  17451  dis2ndc  17480  dislly  17517  llycmpkgen2  17539  cmpkgen  17540  1stckgenlem  17542  1stckgen  17543  ptbasfi  17570  txdis  17621  txdis1cn  17624  txcmplem1  17630  xkohaus  17642  xkoptsub  17643  xkoinjcn  17676  pt1hmeo  17795  snfbas  17855  trnei  17881  isufil2  17897  ufileu  17908  filufint  17909  uffixsn  17914  ufildom1  17915  flimopn  17964  hausflim  17970  flimcf  17971  flimclslem  17973  flimsncls  17975  cnpflf2  17989  cnpflf  17990  fclsneii  18006  fclsfnflim  18016  fcfnei  18024  alexsubALTlem3  18037  alexsubALTlem4  18038  ptcmplem2  18041  cldsubg  18097  snclseqg  18102  divstgphaus  18109  tsmsgsum  18125  tsmsid  18126  tgptsmscld  18137  tsmsxplem1  18139  tsmsxplem2  18140  ust0  18206  ustuqtop1  18228  neipcfilu  18283  prdsdsf  18354  prdsxmetlem  18355  prdsmet  18357  imasdsf1olem  18360  xpsdsval  18368  prdsbl  18478  prdsxmslem2  18516  idnghm  18734  icccmplem2  18811  metnrmlem2  18847  ioombl  19416  volivth  19456  itg11  19540  i1fmulclem  19551  itg2mulclem  19595  itgsplitioo  19686  limcvallem  19715  limcdif  19720  ellimc2  19721  limcflf  19725  limcmpt2  19728  limcres  19730  cnplimc  19731  limccnp  19735  limccnp2  19736  limcco  19737  dvreslem  19753  dvaddbr  19781  dvmulbr  19782  dvcmulf  19788  dvef  19821  dvivth  19851  lhop2  19856  lhop  19857  ply1remlem  20042  fta1blem  20048  ig1peu  20051  ig1pdvds  20056  plyco0  20068  elply2  20072  plyf  20074  elplyr  20077  elplyd  20078  ply1term  20080  ply0  20084  plyeq0lem  20086  plyeq0  20087  plypf1  20088  plyaddlem  20091  plymullem  20092  dgrlem  20105  coef2  20107  coeidlem  20113  plyco  20117  coemulhi  20129  plycj  20152  vieta1  20186  taylf  20234  radcnv0  20289  abelth  20314  rlimcnp  20761  xrlimcnp  20764  amgm  20786  wilthlem2  20809  basellem7  20826  basellem9  20828  ppiprm  20891  chtprm  20893  musumsum  20934  muinv  20935  logexprlim  20966  perfectlem2  20971  dchrhash  21012  rpvmasum2  21163  umgraex  21315  umgra1  21318  uslgra1  21349  usgra1  21350  uvtxnm1nbgra  21460  constr1trl  21545  eupa0  21653  eupap1  21655  0oo  22247  sh0le  22899  kerf1hrm  24219  esumsn  24413  subfacp1lem1  24822  subfacp1lem5  24827  erdszelem4  24837  erdszelem8  24841  sconpi1  24883  cvmscld  24917  cvmlift2lem6  24952  cvmlift2lem9  24955  cvmlift2lem11  24957  cvmlift2lem12  24958  wfrlem15  25488  axlowdimlem7  25795  axlowdimlem10  25798  comppfsc  26281  neibastop2lem  26283  topjoin  26288  fnejoin2  26292  prdsbnd  26396  heiborlem8  26421  rrnequiv  26438  grpokerinj  26454  0idl  26529  prnc  26571  isfldidl  26572  ralxpmap  26636  elrfi  26642  cmpfiiin  26645  mzpcompact2lem  26702  dfac11  27032  pwssplit1  27060  pwssplit4  27063  rngunsnply  27250  flcidc  27251  en2other2  27254  pmtrprfv  27268  acsfn1p  27379  proot1mul  27387  bnj1452  29131  lshpnel2N  29472  lsatfixedN  29496  lfl0f  29556  lkrlsp3  29591  elpaddatriN  30289  elpaddat  30290  elpadd2at  30292  pmodlem1  30332  osumcllem1N  30442  osumcllem2N  30443  osumcllem9N  30450  osumcllem10N  30451  pexmidlem6N  30461  pexmidlem7N  30462  dibss  31656  dochocsn  31868  dochsncom  31869  dochnel  31880  dihprrnlem1N  31911  dihprrnlem2  31912  djhlsmat  31914  dihsmsprn  31917  dvh4dimlem  31930  dvhdimlem  31931  dochsnnz  31937  dochsatshp  31938  dochsnshp  31940  dochexmid  31955  dochsnkr  31959  dochsnkr2cl  31961  dochfl1  31963  lcfl7lem  31986  lcfl6  31987  lcfl8  31989  lcfl9a  31992  lclkrlem2a  31994  lclkrlem2c  31996  lclkrlem2d  31997  lclkrlem2e  31998  lclkrlem2j  32003  lclkrlem2o  32008  lclkrlem2p  32009  lclkrlem2s  32012  lclkrlem2v  32015  lcfrlem14  32043  lcfrlem18  32047  lcfrlem19  32048  lcfrlem20  32049  lcfrlem23  32052  lcfrlem25  32054  lcdlkreqN  32109  mapdval4N  32119  mapdsn  32128  mapdhvmap  32256  hdmaprnlem4tN  32342  hdmapinvlem1  32408  hdmapinvlem2  32409  hdmapinvlem3  32410  hdmapinvlem4  32411  hdmapglem5  32412  hgmapvvlem3  32415  hdmapglem7a  32417  hdmapglem7b  32418  hdmapglem7  32419  hdmapoc  32421
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 2389
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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-in 3291  df-ss 3298  df-sn 3784
  Copyright terms: Public domain W3C validator