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

Theorem snssd 4172
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 4160 . . 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 1767    C_ wss 3476   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115  df-in 3483  df-ss 3490  df-sn 4028
This theorem is referenced by:  frirr  4856  sofld  5453  fr3nr  6593  oeeui  7248  ecinxp  7383  ralxpmap  7465  xpdom3  7612  domunsn  7664  mapdom3  7686  isinf  7730  ac6sfi  7760  pwfilem  7810  finsschain  7823  ssfii  7875  marypha1lem  7889  unxpwdom2  8010  mapfienOLD  8134  en2other2  8383  fseqenlem1  8401  axdc3lem4  8829  axdc4lem  8831  ttukeylem7  8891  fpwwe2lem13  9016  canthwe  9025  canthp1lem1  9026  wuncval2  9121  un0addcl  10825  un0mulcl  10826  fseq1p1m1  11748  hashbclem  12461  hashf1lem1  12464  fsumge1  13567  incexclem  13604  isumltss  13616  rpnnen2lem11  13812  bitsinv1  13944  phicl2  14150  vdwlem1  14351  vdwlem8  14358  vdwlem12  14362  vdwlem13  14363  0ram  14390  ramub1lem1  14396  ramub1lem2  14397  ramcl  14399  imasaddfnlem  14776  imasaddflem  14778  imasvscafn  14785  imasvscaf  14787  mrieqvlemd  14877  mreexmrid  14891  mreexexlem4d  14895  acsfiindd  15657  acsmapd  15658  gsumvallem2  15811  gsumress  15817  0subg  16018  cycsubg2cl  16031  pmtrprfv  16271  odf1o1  16385  gex1  16404  sylow2alem1  16430  sylow2alem2  16431  lsm01  16482  lsm02  16483  lsmdisj  16492  lsmdisj2  16493  prmcyg  16684  gsumzadd  16723  gsumzaddOLD  16725  gsumconst  16742  gsumdifsnd  16775  gsumpt  16776  gsumptOLD  16777  gsumxp  16792  gsumxpOLD  16794  dmdprdd  16818  dprdfadd  16847  dprdfaddOLD  16854  dprdres  16862  dprdz  16864  dprdsn  16870  dprddisj2  16874  dprddisj2OLD  16875  dprd2da  16878  dprd2d2  16880  dmdprdsplit2lem  16881  dpjcntz  16888  dpjdisj  16889  dpjlsm  16890  dpjidcl  16894  dpjidclOLD  16901  ablfacrp  16904  ablfac1eu  16911  pgpfac1lem1  16912  pgpfac1lem3a  16914  pgpfac1lem3  16915  pgpfac1lem5  16917  pgpfaclem2  16920  kerf1hrm  17172  lsssn0  17374  lss0ss  17375  lsptpcl  17405  lspsnvsi  17430  lspun0  17437  pwssplit1  17485  lsmpr  17515  lsppr  17519  lspsntri  17523  lspsolvlem  17568  lspsolv  17569  lsppratlem1  17573  lsppratlem3  17575  lsppratlem4  17576  islbs3  17581  lbsextlem4  17587  rsp1  17651  lidlnz  17655  lidldvgen  17682  psrlidm  17824  psrlidmOLD  17825  psrridm  17826  psrridmOLD  17827  mplmonmul  17894  mulgrhm2  18297  mulgrhm2OLD  18300  zndvds  18352  mdetdiaglem  18864  mdetrlin  18868  mdetrsca  18869  mdetrsca2  18870  mdetrlin2  18873  mdetunilem5  18882  mdetunilem9  18886  mdetmul  18889  en2top  19250  rest0  19433  ordtrest  19466  iscnp4  19527  cnconst2  19547  cnpdis  19557  ist1-2  19611  cnt1  19614  dishaus  19646  discmp  19661  cmpcld  19665  concompid  19695  dis2ndc  19724  dislly  19761  llycmpkgen2  19783  cmpkgen  19784  1stckgenlem  19786  1stckgen  19787  ptbasfi  19814  txdis  19865  txdis1cn  19868  txcmplem1  19874  xkohaus  19886  xkoptsub  19887  xkoinjcn  19920  pt1hmeo  20039  snfbas  20099  trnei  20125  isufil2  20141  ufileu  20152  filufint  20153  uffixsn  20158  ufildom1  20159  flimopn  20208  hausflim  20214  flimcf  20215  flimclslem  20217  flimsncls  20219  cnpflf2  20233  cnpflf  20234  fclsneii  20250  fclsfnflim  20260  fcfnei  20268  alexsubALTlem3  20281  alexsubALTlem4  20282  ptcmplem2  20285  cldsubg  20341  snclseqg  20346  divstgphaus  20353  tsmsgsum  20369  tsmsid  20370  tsmsgsumOLD  20372  tsmsidOLD  20373  tgptsmscld  20385  tsmsxplem1  20387  tsmsxplem2  20388  ust0  20454  ustuqtop1  20476  neipcfilu  20531  prdsdsf  20602  prdsxmetlem  20603  prdsmet  20605  imasdsf1olem  20608  xpsdsval  20616  prdsbl  20726  prdsxmslem2  20764  idnghm  20982  icccmplem2  21060  metnrmlem2  21096  ioombl  21707  volivth  21748  itg11  21830  i1fmulclem  21841  itg2mulclem  21885  itgsplitioo  21976  limcvallem  22007  limcdif  22012  ellimc2  22013  limcflf  22017  limcmpt2  22020  limcres  22022  cnplimc  22023  limccnp  22027  limccnp2  22028  limcco  22029  dvreslem  22045  dvaddbr  22073  dvmulbr  22074  dvcmulf  22080  dvef  22113  dvivth  22143  lhop2  22148  lhop  22149  ply1remlem  22295  fta1blem  22301  ig1peu  22304  ig1pdvds  22309  plyco0  22321  elply2  22325  plyf  22327  elplyr  22330  elplyd  22331  ply1term  22333  ply0  22337  plyeq0lem  22339  plyeq0  22340  plypf1  22341  plyaddlem  22344  plymullem  22345  dgrlem  22358  coef2  22360  coeidlem  22366  plyco  22370  coemulhi  22382  plycj  22405  vieta1  22439  taylf  22487  radcnv0  22542  abelth  22567  rlimcnp  23020  xrlimcnp  23023  amgm  23045  wilthlem2  23068  basellem7  23085  basellem9  23087  ppiprm  23150  chtprm  23152  musumsum  23193  muinv  23194  logexprlim  23225  perfectlem2  23230  dchrhash  23271  rpvmasum2  23422  axlowdimlem7  23924  axlowdimlem10  23927  umgraex  23996  umgra1  23999  uslgra1  24045  usgra1  24046  uvtxnm1nbgra  24167  constr1trl  24263  eupa0  24647  eupap1  24649  0oo  25377  sh0le  26031  ordtrestNEW  27536  qtopt1  27633  esumsn  27709  eulerpartlems  27936  eulerpartlemgc  27938  eulerpartlemgh  27954  eulerpartlemgs2  27956  subfacp1lem1  28260  subfacp1lem5  28265  erdszelem4  28275  erdszelem8  28279  sconpi1  28321  cvmscld  28355  cvmlift2lem6  28390  cvmlift2lem9  28393  cvmlift2lem11  28395  cvmlift2lem12  28396  wfrlem15  28931  comppfsc  29777  neibastop2lem  29779  topjoin  29784  fnejoin2  29788  prdsbnd  29890  heiborlem8  29915  rrnequiv  29932  grpokerinj  29948  0idl  30023  prnc  30065  isfldidl  30066  elrfi  30228  cmpfiiin  30231  mzpcompact2lem  30286  dfac11  30612  pwssplit4  30639  rngunsnply  30727  flcidc  30728  acsfn1p  30753  proot1mul  30761  iocinico  30784  limciccioolb  31163  limcicciooub  31179  limcresiooub  31184  limcresioolb  31185  ioccncflimc  31224  icccncfext  31226  icocncflimc  31228  cncfiooicclem1  31232  cncfiooicc  31233  dirkercncflem2  31404  dirkercncflem3  31405  fourierdlem48  31455  fourierdlem49  31456  fourierdlem101  31508  fsumsplitsndif  31815  gsumdifsndf  32020  bnj1452  33187  lshpnel2N  33782  lsatfixedN  33806  lfl0f  33866  lkrlsp3  33901  elpaddatriN  34599  elpaddat  34600  elpadd2at  34602  pmodlem1  34642  osumcllem1N  34752  osumcllem2N  34753  osumcllem9N  34760  osumcllem10N  34761  pexmidlem6N  34771  pexmidlem7N  34772  dibss  35966  dochocsn  36178  dochsncom  36179  dochnel  36190  dihprrnlem1N  36221  dihprrnlem2  36222  djhlsmat  36224  dihsmsprn  36227  dvh4dimlem  36240  dvhdimlem  36241  dochsnnz  36247  dochsatshp  36248  dochsnshp  36250  dochexmid  36265  dochsnkr  36269  dochsnkr2cl  36271  dochfl1  36273  lcfl7lem  36296  lcfl6  36297  lcfl8  36299  lcfl9a  36302  lclkrlem2a  36304  lclkrlem2c  36306  lclkrlem2d  36307  lclkrlem2e  36308  lclkrlem2j  36313  lclkrlem2o  36318  lclkrlem2p  36319  lclkrlem2s  36322  lclkrlem2v  36325  lcfrlem14  36353  lcfrlem18  36357  lcfrlem19  36358  lcfrlem20  36359  lcfrlem23  36362  lcfrlem25  36364  lcdlkreqN  36419  mapdval4N  36429  mapdsn  36438  mapdhvmap  36566  hdmaprnlem4tN  36652  hdmapinvlem1  36718  hdmapinvlem2  36719  hdmapinvlem3  36720  hdmapinvlem4  36721  hdmapglem5  36722  hgmapvvlem3  36725  hdmapglem7a  36727  hdmapglem7b  36728  hdmapglem7  36729  hdmapoc  36731
  Copyright terms: Public domain W3C validator