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

Theorem snssd 4127
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 4116 . . 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 1758    C_ wss 3437   {csn 3986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080  df-in 3444  df-ss 3451  df-sn 3987
This theorem is referenced by:  frirr  4806  sofld  5395  fr3nr  6502  oeeui  7152  ecinxp  7286  ralxpmap  7373  xpdom3  7520  domunsn  7572  mapdom3  7594  isinf  7638  ac6sfi  7668  pwfilem  7717  finsschain  7730  ssfii  7781  marypha1lem  7795  unxpwdom2  7915  mapfienOLD  8039  en2other2  8288  fseqenlem1  8306  axdc3lem4  8734  axdc4lem  8736  ttukeylem7  8796  fpwwe2lem13  8921  canthwe  8930  canthp1lem1  8931  wuncval2  9026  un0addcl  10725  un0mulcl  10726  fseq1p1m1  11652  hashbclem  12324  hashf1lem1  12327  fsumge1  13379  incexclem  13418  isumltss  13430  rpnnen2lem11  13626  bitsinv1  13757  phicl2  13962  vdwlem1  14161  vdwlem8  14168  vdwlem12  14172  vdwlem13  14173  0ram  14200  ramub1lem1  14206  ramub1lem2  14207  ramcl  14209  imasaddfnlem  14586  imasaddflem  14588  imasvscafn  14595  imasvscaf  14597  mrieqvlemd  14687  mreexmrid  14701  mreexexlem4d  14705  acsfiindd  15467  acsmapd  15468  gsumvallem2  15621  gsumress  15627  0subg  15826  cycsubg2cl  15839  pmtrprfv  16079  odf1o1  16193  gex1  16212  sylow2alem1  16238  sylow2alem2  16239  lsm01  16290  lsm02  16291  lsmdisj  16300  lsmdisj2  16301  prmcyg  16492  gsumzadd  16531  gsumzaddOLD  16533  gsumconst  16550  gsumpt  16577  gsumptOLD  16578  gsumxp  16591  gsumxpOLD  16593  dmdprdd  16604  dprdfadd  16633  dprdfaddOLD  16640  dprdres  16648  dprdz  16650  dprdsn  16656  dprddisj2  16660  dprddisj2OLD  16661  dprd2da  16664  dprd2d2  16666  dmdprdsplit2lem  16667  dpjcntz  16674  dpjdisj  16675  dpjlsm  16676  dpjidcl  16680  dpjidclOLD  16687  ablfacrp  16690  ablfac1eu  16697  pgpfac1lem1  16698  pgpfac1lem3a  16700  pgpfac1lem3  16701  pgpfac1lem5  16703  pgpfaclem2  16706  kerf1hrm  16955  lsssn0  17153  lss0ss  17154  lsptpcl  17184  lspsnvsi  17209  lspun0  17216  pwssplit1  17264  lsmpr  17294  lsppr  17298  lspsntri  17302  lspsolvlem  17347  lspsolv  17348  lsppratlem1  17352  lsppratlem3  17354  lsppratlem4  17355  islbs3  17360  lbsextlem4  17366  rsp1  17430  lidlnz  17434  lidldvgen  17461  psrlidm  17598  psrlidmOLD  17599  psrridm  17600  psrridmOLD  17601  mplmonmul  17668  mulgrhm2  18053  mulgrhm2OLD  18056  zndvds  18108  mdetdiaglem  18537  mdetrlin  18541  mdetrsca  18542  mdetrsca2  18543  mdetrlin2  18546  mdetunilem5  18555  mdetunilem9  18559  mdetmul  18562  en2top  18723  rest0  18906  ordtrest  18939  iscnp4  19000  cnconst2  19020  cnpdis  19030  ist1-2  19084  cnt1  19087  dishaus  19119  discmp  19134  cmpcld  19138  concompid  19168  dis2ndc  19197  dislly  19234  llycmpkgen2  19256  cmpkgen  19257  1stckgenlem  19259  1stckgen  19260  ptbasfi  19287  txdis  19338  txdis1cn  19341  txcmplem1  19347  xkohaus  19359  xkoptsub  19360  xkoinjcn  19393  pt1hmeo  19512  snfbas  19572  trnei  19598  isufil2  19614  ufileu  19625  filufint  19626  uffixsn  19631  ufildom1  19632  flimopn  19681  hausflim  19687  flimcf  19688  flimclslem  19690  flimsncls  19692  cnpflf2  19706  cnpflf  19707  fclsneii  19723  fclsfnflim  19733  fcfnei  19741  alexsubALTlem3  19754  alexsubALTlem4  19755  ptcmplem2  19758  cldsubg  19814  snclseqg  19819  divstgphaus  19826  tsmsgsum  19842  tsmsid  19843  tsmsgsumOLD  19845  tsmsidOLD  19846  tgptsmscld  19858  tsmsxplem1  19860  tsmsxplem2  19861  ust0  19927  ustuqtop1  19949  neipcfilu  20004  prdsdsf  20075  prdsxmetlem  20076  prdsmet  20078  imasdsf1olem  20081  xpsdsval  20089  prdsbl  20199  prdsxmslem2  20237  idnghm  20455  icccmplem2  20533  metnrmlem2  20569  ioombl  21180  volivth  21221  itg11  21303  i1fmulclem  21314  itg2mulclem  21358  itgsplitioo  21449  limcvallem  21480  limcdif  21485  ellimc2  21486  limcflf  21490  limcmpt2  21493  limcres  21495  cnplimc  21496  limccnp  21500  limccnp2  21501  limcco  21502  dvreslem  21518  dvaddbr  21546  dvmulbr  21547  dvcmulf  21553  dvef  21586  dvivth  21616  lhop2  21621  lhop  21622  ply1remlem  21768  fta1blem  21774  ig1peu  21777  ig1pdvds  21782  plyco0  21794  elply2  21798  plyf  21800  elplyr  21803  elplyd  21804  ply1term  21806  ply0  21810  plyeq0lem  21812  plyeq0  21813  plypf1  21814  plyaddlem  21817  plymullem  21818  dgrlem  21831  coef2  21833  coeidlem  21839  plyco  21843  coemulhi  21855  plycj  21878  vieta1  21912  taylf  21960  radcnv0  22015  abelth  22040  rlimcnp  22493  xrlimcnp  22496  amgm  22518  wilthlem2  22541  basellem7  22558  basellem9  22560  ppiprm  22623  chtprm  22625  musumsum  22666  muinv  22667  logexprlim  22698  perfectlem2  22703  dchrhash  22744  rpvmasum2  22895  axlowdimlem7  23347  axlowdimlem10  23350  umgraex  23410  umgra1  23413  uslgra1  23444  usgra1  23445  uvtxnm1nbgra  23555  constr1trl  23640  eupa0  23748  eupap1  23750  0oo  24342  sh0le  24996  ordtrestNEW  26497  esumsn  26661  eulerpartlems  26888  eulerpartlemgc  26890  eulerpartlemgh  26906  eulerpartlemgs2  26908  subfacp1lem1  27212  subfacp1lem5  27217  erdszelem4  27227  erdszelem8  27231  sconpi1  27273  cvmscld  27307  cvmlift2lem6  27342  cvmlift2lem9  27345  cvmlift2lem11  27347  cvmlift2lem12  27348  wfrlem15  27883  comppfsc  28728  neibastop2lem  28730  topjoin  28735  fnejoin2  28739  prdsbnd  28841  heiborlem8  28866  rrnequiv  28883  grpokerinj  28899  0idl  28974  prnc  29016  isfldidl  29017  elrfi  29179  cmpfiiin  29182  mzpcompact2lem  29237  dfac11  29564  pwssplit4  29591  rngunsnply  29679  flcidc  29680  acsfn1p  29705  proot1mul  29713  iocinico  29736  fsumsplitsndif  30387  gsumdifsnd  30911  gsumdifsndf  30914  bnj1452  32376  lshpnel2N  32969  lsatfixedN  32993  lfl0f  33053  lkrlsp3  33088  elpaddatriN  33786  elpaddat  33787  elpadd2at  33789  pmodlem1  33829  osumcllem1N  33939  osumcllem2N  33940  osumcllem9N  33947  osumcllem10N  33948  pexmidlem6N  33958  pexmidlem7N  33959  dibss  35153  dochocsn  35365  dochsncom  35366  dochnel  35377  dihprrnlem1N  35408  dihprrnlem2  35409  djhlsmat  35411  dihsmsprn  35414  dvh4dimlem  35427  dvhdimlem  35428  dochsnnz  35434  dochsatshp  35435  dochsnshp  35437  dochexmid  35452  dochsnkr  35456  dochsnkr2cl  35458  dochfl1  35460  lcfl7lem  35483  lcfl6  35484  lcfl8  35486  lcfl9a  35489  lclkrlem2a  35491  lclkrlem2c  35493  lclkrlem2d  35494  lclkrlem2e  35495  lclkrlem2j  35500  lclkrlem2o  35505  lclkrlem2p  35506  lclkrlem2s  35509  lclkrlem2v  35512  lcfrlem14  35540  lcfrlem18  35544  lcfrlem19  35545  lcfrlem20  35546  lcfrlem23  35549  lcfrlem25  35551  lcdlkreqN  35606  mapdval4N  35616  mapdsn  35625  mapdhvmap  35753  hdmaprnlem4tN  35839  hdmapinvlem1  35905  hdmapinvlem2  35906  hdmapinvlem3  35907  hdmapinvlem4  35908  hdmapglem5  35909  hgmapvvlem3  35912  hdmapglem7a  35914  hdmapglem7b  35915  hdmapglem7  35916  hdmapoc  35918
  Copyright terms: Public domain W3C validator