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

Theorem snssd 4089
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 4077 . . 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 1826    C_ wss 3389   {csn 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-v 3036  df-in 3396  df-ss 3403  df-sn 3945
This theorem is referenced by:  frirr  4770  sofld  5364  fr3nr  6514  oeeui  7169  ecinxp  7304  ralxpmap  7387  xpdom3  7534  domunsn  7586  mapdom3  7608  isinf  7649  ac6sfi  7679  pwfilem  7729  finsschain  7742  ssfii  7794  marypha1lem  7808  unxpwdom2  7929  mapfienOLD  8051  en2other2  8300  fseqenlem1  8318  axdc3lem4  8746  axdc4lem  8748  ttukeylem7  8808  fpwwe2lem13  8931  canthwe  8940  canthp1lem1  8941  wuncval2  9036  un0addcl  10746  un0mulcl  10747  fseq1p1m1  11674  hashbclem  12405  hashf1lem1  12408  fsumge1  13613  incexclem  13650  isumltss  13662  rpnnen2lem11  13960  bitsinv1  14094  phicl2  14300  vdwlem1  14501  vdwlem8  14508  vdwlem12  14512  vdwlem13  14513  0ram  14540  ramub1lem1  14546  ramub1lem2  14547  ramcl  14549  imasaddfnlem  14935  imasaddflem  14937  imasvscafn  14944  imasvscaf  14946  mrieqvlemd  15036  mreexmrid  15050  mreexexlem4d  15054  acsfiindd  15924  acsmapd  15925  gsumress  16020  gsumvallem2  16120  0subg  16343  cycsubg2cl  16356  pmtrprfv  16595  odf1o1  16709  gex1  16728  sylow2alem1  16754  sylow2alem2  16755  lsm01  16806  lsm02  16807  lsmdisj  16816  lsmdisj2  16817  prmcyg  17013  gsumzadd  17052  gsumzaddOLD  17054  gsumconst  17070  gsumdifsnd  17101  gsumpt  17102  gsumptOLD  17103  gsumxp  17118  dmdprdd  17143  dprdfadd  17173  dprdfaddOLD  17180  dprdres  17188  dprdz  17190  dprdsn  17196  dprddisj2  17200  dprddisj2OLD  17201  dprd2da  17204  dprd2d2  17206  dmdprdsplit2lem  17207  dpjcntz  17214  dpjdisj  17215  dpjlsm  17216  dpjidcl  17220  dpjidclOLD  17227  ablfacrp  17230  ablfac1eu  17237  pgpfac1lem1  17238  pgpfac1lem3a  17240  pgpfac1lem3  17241  pgpfac1lem5  17243  pgpfaclem2  17246  kerf1hrm  17505  lsssn0  17707  lss0ss  17708  lsptpcl  17738  lspsnvsi  17763  lspun0  17770  pwssplit1  17818  lsmpr  17848  lsppr  17852  lspsntri  17856  lspsolvlem  17901  lspsolv  17902  lsppratlem1  17906  lsppratlem3  17908  lsppratlem4  17909  islbs3  17914  lbsextlem4  17920  rsp1  17985  lidlnz  17989  lidldvgen  18016  psrlidm  18169  psrlidmOLD  18170  psrridm  18171  psrridmOLD  18172  mplmonmul  18239  mulgrhm2  18629  zndvds  18679  mdetdiaglem  19185  mdetrlin  19189  mdetrsca  19190  mdetrsca2  19191  mdetrlin2  19194  mdetunilem5  19203  mdetunilem9  19207  mdetmul  19210  en2top  19572  rest0  19756  ordtrest  19789  iscnp4  19850  cnconst2  19870  cnpdis  19880  ist1-2  19934  cnt1  19937  dishaus  19969  discmp  19984  cmpcld  19988  concompid  20017  dis2ndc  20046  dislly  20083  dissnref  20114  comppfsc  20118  llycmpkgen2  20136  cmpkgen  20137  1stckgenlem  20139  1stckgen  20140  ptbasfi  20167  txdis  20218  txdis1cn  20221  txcmplem1  20227  xkohaus  20239  xkoptsub  20240  xkoinjcn  20273  pt1hmeo  20392  snfbas  20452  trnei  20478  isufil2  20494  ufileu  20505  filufint  20506  uffixsn  20511  ufildom1  20512  flimopn  20561  hausflim  20567  flimcf  20568  flimclslem  20570  flimsncls  20572  cnpflf2  20586  cnpflf  20587  fclsneii  20603  fclsfnflim  20613  fcfnei  20621  alexsubALTlem3  20634  alexsubALTlem4  20635  ptcmplem2  20638  cldsubg  20694  snclseqg  20699  qustgphaus  20706  tsmsgsum  20722  tsmsid  20723  tsmsgsumOLD  20725  tsmsidOLD  20726  tgptsmscld  20738  tsmsxplem1  20740  tsmsxplem2  20741  ust0  20807  ustuqtop1  20829  neipcfilu  20884  prdsdsf  20955  prdsxmetlem  20956  prdsmet  20958  imasdsf1olem  20961  xpsdsval  20969  prdsbl  21079  prdsxmslem2  21117  idnghm  21335  icccmplem2  21413  metnrmlem2  21449  ioombl  22060  volivth  22101  itg11  22183  i1fmulclem  22194  itg2mulclem  22238  itgsplitioo  22329  limcvallem  22360  limcdif  22365  ellimc2  22366  limcflf  22370  limcmpt2  22373  limcres  22375  cnplimc  22376  limccnp  22380  limccnp2  22381  limcco  22382  dvreslem  22398  dvaddbr  22426  dvmulbr  22427  dvcmulf  22433  dvef  22466  dvivth  22496  lhop2  22501  lhop  22502  ply1remlem  22648  fta1blem  22654  ig1peu  22657  ig1pdvds  22662  plyco0  22674  elply2  22678  plyf  22680  elplyr  22683  elplyd  22684  ply1term  22686  ply0  22690  plyeq0lem  22692  plyeq0  22693  plypf1  22694  plyaddlem  22697  plymullem  22698  dgrlem  22711  coef2  22713  coeidlem  22719  plyco  22723  coemulhi  22736  plycj  22759  vieta1  22793  taylf  22841  radcnv0  22896  abelth  22921  rlimcnp  23412  xrlimcnp  23415  amgm  23437  wilthlem2  23460  basellem7  23477  basellem9  23479  ppiprm  23542  chtprm  23544  musumsum  23585  muinv  23586  logexprlim  23617  perfectlem2  23622  dchrhash  23663  rpvmasum2  23814  axlowdimlem7  24372  axlowdimlem10  24375  umgraex  24444  umgra1  24447  uslgra1  24493  usgra1  24494  uvtxnm1nbgra  24615  constr1trl  24711  eupa0  25095  eupap1  25097  0oo  25821  sh0le  26475  disjiunel  27585  qtopt1  27992  locfinref  27998  ordtrestNEW  28057  esumsnf  28212  carsggect  28445  eulerpartlems  28482  eulerpartlemgc  28484  eulerpartlemgh  28500  eulerpartlemgs2  28502  plymulx0  28687  subfacp1lem1  28812  subfacp1lem5  28817  erdszelem4  28827  erdszelem8  28831  sconpi1  28873  cvmscld  28907  cvmlift2lem6  28942  cvmlift2lem9  28945  cvmlift2lem11  28947  cvmlift2lem12  28948  mrsubvrs  29071  wfrlem15  29522  neibastop2lem  30344  topjoin  30349  fnejoin2  30353  prdsbnd  30455  heiborlem8  30480  rrnequiv  30497  grpokerinj  30513  0idl  30588  prnc  30630  isfldidl  30631  elrfi  30792  cmpfiiin  30795  mzpcompact2lem  30849  dfac11  31174  pwssplit4  31201  rngunsnply  31290  flcidc  31291  acsfn1p  31316  proot1mul  31324  iocinico  31347  binomcxplemnn0  31422  fsumsplit1  31739  islptre  31791  limciccioolb  31793  limcicciooub  31809  limcresiooub  31814  limcresioolb  31815  ioccncflimc  31854  icccncfext  31856  icocncflimc  31858  cncfiooicc  31863  dvnprodlem2  31910  dirkercncflem2  32052  dirkercncflem3  32053  fourierdlem48  32103  fourierdlem49  32104  fourierdlem79  32134  fourierdlem101  32156  perfectALTVlem2  32544  fsumsplitsndif  32664  gsumdifsndf  33155  bnj1452  34455  lshpnel2N  35123  lsatfixedN  35147  lfl0f  35207  lkrlsp3  35242  elpaddatriN  35940  elpaddat  35941  elpadd2at  35943  pmodlem1  35983  osumcllem1N  36093  osumcllem2N  36094  osumcllem9N  36101  osumcllem10N  36102  pexmidlem6N  36112  pexmidlem7N  36113  dibss  37309  dochocsn  37521  dochsncom  37522  dochnel  37533  dihprrnlem1N  37564  dihprrnlem2  37565  djhlsmat  37567  dihsmsprn  37570  dvh4dimlem  37583  dvhdimlem  37584  dochsnnz  37590  dochsatshp  37591  dochsnshp  37593  dochexmid  37608  dochsnkr  37612  dochsnkr2cl  37614  dochfl1  37616  lcfl7lem  37639  lcfl6  37640  lcfl8  37642  lcfl9a  37645  lclkrlem2a  37647  lclkrlem2c  37649  lclkrlem2d  37650  lclkrlem2e  37651  lclkrlem2j  37656  lclkrlem2o  37661  lclkrlem2p  37662  lclkrlem2s  37665  lclkrlem2v  37668  lcfrlem14  37696  lcfrlem18  37700  lcfrlem19  37701  lcfrlem20  37702  lcfrlem23  37705  lcfrlem25  37707  lcdlkreqN  37762  mapdval4N  37772  mapdsn  37781  mapdhvmap  37909  hdmaprnlem4tN  37995  hdmapinvlem1  38061  hdmapinvlem2  38062  hdmapinvlem3  38063  hdmapinvlem4  38064  hdmapglem5  38065  hgmapvvlem3  38068  hdmapglem7a  38070  hdmapglem7b  38071  hdmapglem7  38072  hdmapoc  38074  iunrelexp0  38242
  Copyright terms: Public domain W3C validator