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

Theorem snssd 3945
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 3934 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 203 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    e. wcel 1726    C_ wss 3322   {csn 3816
This theorem is referenced by:  frirr  4562  fr3nr  4763  sofld  5321  oeeui  6848  ecinxp  6982  xpdom3  7209  domunsn  7260  mapdom3  7282  isinf  7325  ac6sfi  7354  pwfilem  7404  finsschain  7416  ssfii  7427  marypha1lem  7441  unxpwdom2  7559  mapfien  7656  fseqenlem1  7910  axdc3lem4  8338  axdc4lem  8340  ttukeylem7  8400  fpwwe2lem13  8522  canthwe  8531  canthp1lem1  8532  wuncval2  8627  un0addcl  10258  un0mulcl  10259  fseq1p1m1  11127  hashbclem  11706  hashf1lem1  11709  fsumge1  12581  incexclem  12621  isumltss  12633  rpnnen2lem11  12829  bitsinv1  12959  phicl2  13162  vdwlem1  13354  vdwlem8  13361  vdwlem12  13365  vdwlem13  13366  0ram  13393  ramub1lem1  13399  ramub1lem2  13400  ramcl  13402  imasaddfnlem  13758  imasaddflem  13760  imasvscafn  13767  imasvscaf  13769  mrieqvlemd  13859  mreexmrid  13873  mreexexlem4d  13877  acsfiindd  14608  acsmapd  14609  gsumvallem2  14777  gsumress  14782  0subg  14970  cycsubg2cl  14983  odf1o1  15211  gex1  15230  sylow2alem1  15256  sylow2alem2  15257  lsm01  15308  lsm02  15309  lsmdisj  15318  lsmdisj2  15319  prmcyg  15508  gsumzadd  15532  gsumconst  15537  gsumpt  15550  gsumxp  15555  dmdprdd  15565  dprdfadd  15583  dprdres  15591  dprdz  15593  dprdsn  15599  dprddisj2  15602  dprd2da  15605  dprd2d2  15607  dmdprdsplit2lem  15608  dpjcntz  15615  dpjdisj  15616  dpjlsm  15617  dpjidcl  15621  ablfacrp  15629  ablfac1eu  15636  pgpfac1lem1  15637  pgpfac1lem3a  15639  pgpfac1lem3  15640  pgpfac1lem5  15642  pgpfaclem2  15645  lsssn0  16029  lss0ss  16030  lsptpcl  16060  lspsnvsi  16085  lspun0  16092  lsmpr  16166  lsppr  16170  lspsntri  16174  lspsolvlem  16219  lspsolv  16220  lsppratlem1  16224  lsppratlem3  16226  lsppratlem4  16227  islbs3  16232  lbsextlem4  16238  rsp1  16300  lidlnz  16304  lidldvgen  16331  psrlidm  16472  psrridm  16473  mplmonmul  16532  mulgrhm2  16793  zndvds  16835  en2top  17055  rest0  17238  ordtrest  17271  iscnp4  17332  cnconst2  17352  cnpdis  17362  ist1-2  17416  cnt1  17419  dishaus  17451  discmp  17466  cmpcld  17470  concompid  17499  dis2ndc  17528  dislly  17565  llycmpkgen2  17587  cmpkgen  17588  1stckgenlem  17590  1stckgen  17591  ptbasfi  17618  txdis  17669  txdis1cn  17672  txcmplem1  17678  xkohaus  17690  xkoptsub  17691  xkoinjcn  17724  pt1hmeo  17843  snfbas  17903  trnei  17929  isufil2  17945  ufileu  17956  filufint  17957  uffixsn  17962  ufildom1  17963  flimopn  18012  hausflim  18018  flimcf  18019  flimclslem  18021  flimsncls  18023  cnpflf2  18037  cnpflf  18038  fclsneii  18054  fclsfnflim  18064  fcfnei  18072  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem2  18089  cldsubg  18145  snclseqg  18150  divstgphaus  18157  tsmsgsum  18173  tsmsid  18174  tgptsmscld  18185  tsmsxplem1  18187  tsmsxplem2  18188  ust0  18254  ustuqtop1  18276  neipcfilu  18331  prdsdsf  18402  prdsxmetlem  18403  prdsmet  18405  imasdsf1olem  18408  xpsdsval  18416  prdsbl  18526  prdsxmslem2  18564  idnghm  18782  icccmplem2  18859  metnrmlem2  18895  ioombl  19464  volivth  19504  itg11  19586  i1fmulclem  19597  itg2mulclem  19641  itgsplitioo  19732  limcvallem  19763  limcdif  19768  ellimc2  19769  limcflf  19773  limcmpt2  19776  limcres  19778  cnplimc  19779  limccnp  19783  limccnp2  19784  limcco  19785  dvreslem  19801  dvaddbr  19829  dvmulbr  19830  dvcmulf  19836  dvef  19869  dvivth  19899  lhop2  19904  lhop  19905  ply1remlem  20090  fta1blem  20096  ig1peu  20099  ig1pdvds  20104  plyco0  20116  elply2  20120  plyf  20122  elplyr  20125  elplyd  20126  ply1term  20128  ply0  20132  plyeq0lem  20134  plyeq0  20135  plypf1  20136  plyaddlem  20139  plymullem  20140  dgrlem  20153  coef2  20155  coeidlem  20161  plyco  20165  coemulhi  20177  plycj  20200  vieta1  20234  taylf  20282  radcnv0  20337  abelth  20362  rlimcnp  20809  xrlimcnp  20812  amgm  20834  wilthlem2  20857  basellem7  20874  basellem9  20876  ppiprm  20939  chtprm  20941  musumsum  20982  muinv  20983  logexprlim  21014  perfectlem2  21019  dchrhash  21060  rpvmasum2  21211  umgraex  21363  umgra1  21366  uslgra1  21397  usgra1  21398  uvtxnm1nbgra  21508  constr1trl  21593  eupa0  21701  eupap1  21703  0oo  22295  sh0le  22947  kerf1hrm  24267  esumsn  24461  subfacp1lem1  24870  subfacp1lem5  24875  erdszelem4  24885  erdszelem8  24889  sconpi1  24931  cvmscld  24965  cvmlift2lem6  25000  cvmlift2lem9  25003  cvmlift2lem11  25005  cvmlift2lem12  25006  wfrlem15  25557  axlowdimlem7  25892  axlowdimlem10  25895  comppfsc  26401  neibastop2lem  26403  topjoin  26408  fnejoin2  26412  prdsbnd  26516  heiborlem8  26541  rrnequiv  26558  grpokerinj  26574  0idl  26649  prnc  26691  isfldidl  26692  ralxpmap  26756  elrfi  26762  cmpfiiin  26765  mzpcompact2lem  26822  dfac11  27151  pwssplit1  27179  pwssplit4  27182  rngunsnply  27369  flcidc  27370  en2other2  27373  pmtrprfv  27387  acsfn1p  27498  proot1mul  27506  bnj1452  29495  lshpnel2N  29857  lsatfixedN  29881  lfl0f  29941  lkrlsp3  29976  elpaddatriN  30674  elpaddat  30675  elpadd2at  30677  pmodlem1  30717  osumcllem1N  30827  osumcllem2N  30828  osumcllem9N  30835  osumcllem10N  30836  pexmidlem6N  30846  pexmidlem7N  30847  dibss  32041  dochocsn  32253  dochsncom  32254  dochnel  32265  dihprrnlem1N  32296  dihprrnlem2  32297  djhlsmat  32299  dihsmsprn  32302  dvh4dimlem  32315  dvhdimlem  32316  dochsnnz  32322  dochsatshp  32323  dochsnshp  32325  dochexmid  32340  dochsnkr  32344  dochsnkr2cl  32346  dochfl1  32348  lcfl7lem  32371  lcfl6  32372  lcfl8  32374  lcfl9a  32377  lclkrlem2a  32379  lclkrlem2c  32381  lclkrlem2d  32382  lclkrlem2e  32383  lclkrlem2j  32388  lclkrlem2o  32393  lclkrlem2p  32394  lclkrlem2s  32397  lclkrlem2v  32400  lcfrlem14  32428  lcfrlem18  32432  lcfrlem19  32433  lcfrlem20  32434  lcfrlem23  32437  lcfrlem25  32439  lcdlkreqN  32494  mapdval4N  32504  mapdsn  32513  mapdhvmap  32641  hdmaprnlem4tN  32727  hdmapinvlem1  32793  hdmapinvlem2  32794  hdmapinvlem3  32795  hdmapinvlem4  32796  hdmapglem5  32797  hgmapvvlem3  32800  hdmapglem7a  32802  hdmapglem7b  32803  hdmapglem7  32804  hdmapoc  32806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336  df-sn 3822
  Copyright terms: Public domain W3C validator