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

Theorem snssd 4013
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 4002 . . 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 1756    C_ wss 3323   {csn 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2969  df-in 3330  df-ss 3337  df-sn 3873
This theorem is referenced by:  frirr  4692  sofld  5281  fr3nr  6386  oeeui  7033  ecinxp  7167  ralxpmap  7254  xpdom3  7401  domunsn  7453  mapdom3  7475  isinf  7518  ac6sfi  7548  pwfilem  7597  finsschain  7610  ssfii  7661  marypha1lem  7675  unxpwdom2  7795  mapfienOLD  7919  en2other2  8168  fseqenlem1  8186  axdc3lem4  8614  axdc4lem  8616  ttukeylem7  8676  fpwwe2lem13  8801  canthwe  8810  canthp1lem1  8811  wuncval2  8906  un0addcl  10605  un0mulcl  10606  fseq1p1m1  11526  hashbclem  12197  hashf1lem1  12200  fsumge1  13252  incexclem  13291  isumltss  13303  rpnnen2lem11  13499  bitsinv1  13630  phicl2  13835  vdwlem1  14034  vdwlem8  14041  vdwlem12  14045  vdwlem13  14046  0ram  14073  ramub1lem1  14079  ramub1lem2  14080  ramcl  14082  imasaddfnlem  14458  imasaddflem  14460  imasvscafn  14467  imasvscaf  14469  mrieqvlemd  14559  mreexmrid  14573  mreexexlem4d  14577  acsfiindd  15339  acsmapd  15340  gsumvallem2  15492  gsumress  15498  0subg  15697  cycsubg2cl  15710  pmtrprfv  15950  odf1o1  16062  gex1  16081  sylow2alem1  16107  sylow2alem2  16108  lsm01  16159  lsm02  16160  lsmdisj  16169  lsmdisj2  16170  prmcyg  16361  gsumzadd  16400  gsumzaddOLD  16402  gsumconst  16417  gsumpt  16443  gsumptOLD  16444  gsumxp  16456  gsumxpOLD  16458  dmdprdd  16469  dprdfadd  16498  dprdfaddOLD  16505  dprdres  16513  dprdz  16515  dprdsn  16521  dprddisj2  16525  dprddisj2OLD  16526  dprd2da  16529  dprd2d2  16531  dmdprdsplit2lem  16532  dpjcntz  16539  dpjdisj  16540  dpjlsm  16541  dpjidcl  16545  dpjidclOLD  16552  ablfacrp  16555  ablfac1eu  16562  pgpfac1lem1  16563  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfac1lem5  16568  pgpfaclem2  16571  lsssn0  17006  lss0ss  17007  lsptpcl  17037  lspsnvsi  17062  lspun0  17069  pwssplit1  17117  lsmpr  17147  lsppr  17151  lspsntri  17155  lspsolvlem  17200  lspsolv  17201  lsppratlem1  17205  lsppratlem3  17207  lsppratlem4  17208  islbs3  17213  lbsextlem4  17219  rsp1  17283  lidlnz  17287  lidldvgen  17314  psrlidm  17451  psrlidmOLD  17452  psrridm  17453  psrridmOLD  17454  mplmonmul  17520  mulgrhm2  17902  mulgrhm2OLD  17905  zndvds  17957  mdet1  18383  mdetrlin  18384  mdetrsca  18385  mdetrsca2  18386  mdetrlin2  18388  mdetunilem5  18397  mdetunilem9  18401  mdetmul  18404  en2top  18565  rest0  18748  ordtrest  18781  iscnp4  18842  cnconst2  18862  cnpdis  18872  ist1-2  18926  cnt1  18929  dishaus  18961  discmp  18976  cmpcld  18980  concompid  19010  dis2ndc  19039  dislly  19076  llycmpkgen2  19098  cmpkgen  19099  1stckgenlem  19101  1stckgen  19102  ptbasfi  19129  txdis  19180  txdis1cn  19183  txcmplem1  19189  xkohaus  19201  xkoptsub  19202  xkoinjcn  19235  pt1hmeo  19354  snfbas  19414  trnei  19440  isufil2  19456  ufileu  19467  filufint  19468  uffixsn  19473  ufildom1  19474  flimopn  19523  hausflim  19529  flimcf  19530  flimclslem  19532  flimsncls  19534  cnpflf2  19548  cnpflf  19549  fclsneii  19565  fclsfnflim  19575  fcfnei  19583  alexsubALTlem3  19596  alexsubALTlem4  19597  ptcmplem2  19600  cldsubg  19656  snclseqg  19661  divstgphaus  19668  tsmsgsum  19684  tsmsid  19685  tsmsgsumOLD  19687  tsmsidOLD  19688  tgptsmscld  19700  tsmsxplem1  19702  tsmsxplem2  19703  ust0  19769  ustuqtop1  19791  neipcfilu  19846  prdsdsf  19917  prdsxmetlem  19918  prdsmet  19920  imasdsf1olem  19923  xpsdsval  19931  prdsbl  20041  prdsxmslem2  20079  idnghm  20297  icccmplem2  20375  metnrmlem2  20411  ioombl  21021  volivth  21062  itg11  21144  i1fmulclem  21155  itg2mulclem  21199  itgsplitioo  21290  limcvallem  21321  limcdif  21326  ellimc2  21327  limcflf  21331  limcmpt2  21334  limcres  21336  cnplimc  21337  limccnp  21341  limccnp2  21342  limcco  21343  dvreslem  21359  dvaddbr  21387  dvmulbr  21388  dvcmulf  21394  dvef  21427  dvivth  21457  lhop2  21462  lhop  21463  ply1remlem  21609  fta1blem  21615  ig1peu  21618  ig1pdvds  21623  plyco0  21635  elply2  21639  plyf  21641  elplyr  21644  elplyd  21645  ply1term  21647  ply0  21651  plyeq0lem  21653  plyeq0  21654  plypf1  21655  plyaddlem  21658  plymullem  21659  dgrlem  21672  coef2  21674  coeidlem  21680  plyco  21684  coemulhi  21696  plycj  21719  vieta1  21753  taylf  21801  radcnv0  21856  abelth  21881  rlimcnp  22334  xrlimcnp  22337  amgm  22359  wilthlem2  22382  basellem7  22399  basellem9  22401  ppiprm  22464  chtprm  22466  musumsum  22507  muinv  22508  logexprlim  22539  perfectlem2  22544  dchrhash  22585  rpvmasum2  22736  axlowdimlem7  23145  axlowdimlem10  23148  umgraex  23208  umgra1  23211  uslgra1  23242  usgra1  23243  uvtxnm1nbgra  23353  constr1trl  23438  eupa0  23546  eupap1  23548  0oo  24140  sh0le  24794  kerf1hrm  26243  ordtrestNEW  26303  esumsn  26467  eulerpartlems  26695  eulerpartlemgc  26697  eulerpartlemgh  26713  eulerpartlemgs2  26715  subfacp1lem1  27019  subfacp1lem5  27024  erdszelem4  27034  erdszelem8  27038  sconpi1  27080  cvmscld  27114  cvmlift2lem6  27149  cvmlift2lem9  27152  cvmlift2lem11  27154  cvmlift2lem12  27155  wfrlem15  27689  comppfsc  28532  neibastop2lem  28534  topjoin  28539  fnejoin2  28543  prdsbnd  28645  heiborlem8  28670  rrnequiv  28687  grpokerinj  28703  0idl  28778  prnc  28820  isfldidl  28821  elrfi  28983  cmpfiiin  28986  mzpcompact2lem  29041  dfac11  29368  pwssplit4  29395  rngunsnply  29483  flcidc  29484  acsfn1p  29509  proot1mul  29517  iocinico  29540  fsumsplitsndif  30191  gsumdifsnd  30713  gsumdifsndf  30716  mdetdiaglem  30824  bnj1452  31930  lshpnel2N  32470  lsatfixedN  32494  lfl0f  32554  lkrlsp3  32589  elpaddatriN  33287  elpaddat  33288  elpadd2at  33290  pmodlem1  33330  osumcllem1N  33440  osumcllem2N  33441  osumcllem9N  33448  osumcllem10N  33449  pexmidlem6N  33459  pexmidlem7N  33460  dibss  34654  dochocsn  34866  dochsncom  34867  dochnel  34878  dihprrnlem1N  34909  dihprrnlem2  34910  djhlsmat  34912  dihsmsprn  34915  dvh4dimlem  34928  dvhdimlem  34929  dochsnnz  34935  dochsatshp  34936  dochsnshp  34938  dochexmid  34953  dochsnkr  34957  dochsnkr2cl  34959  dochfl1  34961  lcfl7lem  34984  lcfl6  34985  lcfl8  34987  lcfl9a  34990  lclkrlem2a  34992  lclkrlem2c  34994  lclkrlem2d  34995  lclkrlem2e  34996  lclkrlem2j  35001  lclkrlem2o  35006  lclkrlem2p  35007  lclkrlem2s  35010  lclkrlem2v  35013  lcfrlem14  35041  lcfrlem18  35045  lcfrlem19  35046  lcfrlem20  35047  lcfrlem23  35050  lcfrlem25  35052  lcdlkreqN  35107  mapdval4N  35117  mapdsn  35126  mapdhvmap  35254  hdmaprnlem4tN  35340  hdmapinvlem1  35406  hdmapinvlem2  35407  hdmapinvlem3  35408  hdmapinvlem4  35409  hdmapglem5  35410  hgmapvvlem3  35413  hdmapglem7a  35415  hdmapglem7b  35416  hdmapglem7  35417  hdmapoc  35419
  Copyright terms: Public domain W3C validator