Theorem snssd 4757

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
snssd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Assertion

Ref	Expression
snssd	⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		snssi 4756	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-sn 4595

This theorem is referenced by:  intidg  5439  sofld  6186  fsnex  7282  fr3nr  7771  resf1extb  7931  resf1ext2b  7932  frrlem13  8295  oeeui  8588  naddunif  8680  naddasslem1  8681  naddasslem2  8682  ecinxp  8790  ralxpmap  8894  xpdom3  9063  domunsn  9115  mapdom3  9137  isinf  9225  ac6sfi  9244  pwfilem  9277  finsschain  9316  ssfii  9379  marypha1lem  9393  unxpwdom2  9550  en2other2  9993  fseqenlem1  10008  axdc3lem4  10437  axdc4lem  10439  ttukeylem7  10499  fpwwe2lem12  10627  canthwe  10636  canthp1lem1  10637  wuncval2  10732  un0addcl  12537  un0mulcl  12538  ssfzunsnext  13597  fseq1p1m1  13626  hashbclem  14489  hashf1lem1  14492  fsumsplit1  15796  fsumge1  15849  incexclem  15890  isumltss  15902  fprodsplit1f  16044  rpnnen2lem11  16280  bitsinv1  16500  lcmfunsnlem2  16698  lcmfass  16704  phicl2  16827  vdwlem1  17041  vdwlem8  17048  vdwlem12  17052  vdwlem13  17053  0ram  17080  ramub1lem1  17086  ramub1lem2  17087  ramcl  17089  imasaddfnlem  17582  imasaddflem  17584  imasvscafn  17591  imasvscaf  17593  mrieqvlemd  17685  mreexmrid  17699  mreexexlem4d  17703  acsfiindd  18609  acsmapd  18610  chnccat  18682  gsumress  18740  0subm  18876  gsumvallem2  18893  trivsubgd  19219  trivsubgsnd  19220  trivnsgd  19238  cycsubg2cl  19282  kerf1ghm  19317  pmtrprfv  19523  odf1o1  19642  gex1  19661  sylow2alem1  19687  sylow2alem2  19688  lsm01  19741  lsm02  19742  lsmdisj  19751  lsmdisj2  19752  prmcyg  19964  gsumzadd  19992  gsumconst  20004  gsumdifsnd  20031  gsumpt  20032  gsumxp  20046  dmdprdd  20071  dprdfadd  20092  dprdres  20100  dprdz  20102  dprdsn  20108  dprddisj2  20111  dprd2da  20114  dprd2d2  20116  dmdprdsplit2lem  20117  dpjcntz  20124  dpjdisj  20125  dpjlsm  20126  dpjidcl  20130  ablfacrp  20138  ablfac1eu  20145  pgpfac1lem1  20146  pgpfac1lem3a  20148  pgpfac1lem3  20149  pgpfac1lem5  20151  pgpfaclem2  20154  acsfn1p  20880  lsssn0  21047  lss0ss  21048  lsptpcl  21078  lspsnvsi  21103  lspun0  21110  pwssplit1  21158  lsmpr  21188  lsppr  21192  lspsntri  21196  lspsolvlem  21244  lspsolv  21245  lsppratlem1  21249  lsppratlem3  21251  lsppratlem4  21252  islbs3  21257  lbsextlem4  21263  rnglidl0  21333  0ringidl  21338  rsp1  21344  lidlnz  21350  isprmidlc  21443  qsidomlem2  21450  ssdifidlprm  21455  lidldvgen  21471  mulgrhm2  21597  zndvds  21668  psrlidm  22080  psrridm  22081  mplmonmul  22156  selvvvval  22262  mdetdiaglem  22724  mdetrlin  22728  mdetrsca  22729  mdetrsca2  22730  mdetrlin2  22733  mdetunilem5  22742  mdetunilem9  22746  mdetmul  22749  en2top  23111  rest0  23295  ordtrest  23328  iscnp4  23389  cnconst2  23409  cnpdis  23419  ist1-2  23473  cnt1  23476  dishaus  23508  discmp  23524  cmpcld  23528  conncompid  23557  dis2ndc  23586  dislly  23623  dissnref  23654  comppfsc  23658  llycmpkgen2  23676  cmpkgen  23677  1stckgenlem  23679  1stckgen  23680  ptbasfi  23707  txdis  23758  txdis1cn  23761  txcmplem1  23767  xkohaus  23779  xkoptsub  23780  xkoinjcn  23813  snfbas  23992  trnei  24018  isufil2  24034  ufileu  24045  filufint  24046  uffixsn  24051  ufildom1  24052  flimopn  24101  hausflim  24107  flimcf  24108  flimclslem  24110  flimsncls  24112  cnpflf2  24126  cnpflf  24127  fclsneii  24143  fclsfnflim  24153  fcfnei  24161  flfcntr  24169  alexsubALTlem3  24175  alexsubALTlem4  24176  ptcmplem2  24179  cldsubg  24237  snclseqg  24242  qustgphaus  24249  tsmsgsum  24265  tsmsid  24266  tgptsmscld  24277  tsmsxplem1  24279  tsmsxplem2  24280  ust0  24346  ustuqtop1  24367  neipcfilu  24421  prdsdsf  24493  prdsxmetlem  24494  prdsmet  24496  imasdsf1olem  24499  xpsdsval  24507  prdsbl  24617  prdsxmslem2  24655  idnghm  24869  icccmplem2  24950  metnrmlem2  24987  ioombl  25693  volivth  25735  itg11  25819  i1fmulclem  25830  itg2mulclem  25874  itgsplitioo  25966  limcvallem  25999  limcdif  26004  ellimc2  26005  limcflf  26009  limcmpt2  26012  limcres  26014  cnplimc  26015  limccnp  26019  limccnp2  26020  limcco  26021  dvreslem  26037  dvaddbr  26066  dvmulbr  26067  dvcmulf  26073  dvef  26108  dvivth  26138  lhop2  26143  lhop  26144  ply1remlem  26291  fta1blem  26297  ig1peu  26301  ig1pdvds  26306  plyco0  26318  elply2  26322  plyf  26324  elplyr  26327  elplyd  26328  ply1term  26330  ply0  26334  plyeq0lem  26336  plyeq0  26337  plypf1  26338  plyaddlem  26341  plymullem  26342  dgrlem  26355  coef2  26357  coeidlem  26363  plyco  26367  coemulhi  26380  plycj  26403  plycjOLD  26405  plyn0mulidp  26411  vieta1  26442  taylf  26490  radcnv0  26545  abelth  26570  rlimcnp  27096  xrlimcnp  27099  amgm  27121  wilthlem2  27199  basellem7  27217  basellem9  27219  ppiprm  27281  chtprm  27283  musumsum  27322  muinv  27323  logexprlim  27355  perfectlem2  27360  dchrhash  27401  rpvmasum2  27642  sltssnb  27928  conway  27938  lesrec  27958  eqcuts3  27963  cofcutr  28083  cutlt  28091  cutmax  28093  cutmin  28094  cutminmax  28095  addsuniflem  28160  negsunif  28214  sltmuls1  28306  sltmuls2  28307  precsexlem11  28376  oncutlt  28423  n0fincut  28514  bdaypw2n0bndlem  28622  axlowdimlem7  29239  axlowdimlem10  29242  upgrex  29383  upgr1elem  29403  uvtxnm1nbgr  29695  umgr2v2e  29816  cyclnumvtx  30090  0oo  31082  sh0le  31733  disjiunel  32882  preimane  32955  fnpreimac  32956  fsuppinisegfi  32973  fprodeq02  33109  indsn  33124  s1f1  33204  gsumzresunsn  33323  gsumhashmul  33328  pmtrcnelor  33352  primefldgen1  33585  dvdsrspss  33644  elgrplsmsn  33647  lsmsnorb  33648  grplsm0l  33656  grplsmid  33657  unitpidl1  33676  elrspunsn  33681  drngidl  33685  mxidlprm  33698  mxidlirredi  33699  mxidlirred  33700  drngmxidl  33704  drngmxidlr  33705  qsdrngilem  33721  dflringlem  33729  rsprprmprmidl  33757  rprmirredb  33767  1arithufdlem4  33782  selvply1rhmlem1  33855  selvply1rhmlem2  33856  selvply1rhmlem4  33858  selvply1rhmlem5  33859  selvply1rhm  33860  selvply1rhm0  33861  mvrvalind  33873  mplmulmvr  33874  evlextv  33877  psrmonmul  33885  esplyfval0  33899  esplyfvaln  33909  esplyind  33910  esplyindfv  33911  vietalem  33914  lsatdim  33952  drngdimgt0  33953  dimkerim  33962  evls1fldgencl  34005  algextdeglem1  34052  algextdeglem2  34053  algextdeglem3  34054  algextdeglem4  34055  algextdeglem5  34056  rtelextdg2  34062  constrextdg2lem  34083  constrext2chnlem  34085  constrfiss  34086  qtopt1  34170  locfinref  34176  zarcls0  34203  zarmxt1  34215  zarcmplem  34216  ordtrestNEW  34256  esumsnf  34399  esum2dlem  34427  rossros  34515  oms0  34632  carsggect  34653  eulerpartlems  34695  eulerpartlemgc  34697  eulerpartlemgh  34713  eulerpartlemgs2  34715  circlemeth  34972  hgt750lemb  34988  hgt750leme  34990  bnj1452  35385  pthhashvtx  35519  subfacp1lem1  35570  subfacp1lem5  35575  erdszelem4  35585  erdszelem8  35589  sconnpi1  35630  cvmscld  35664  cvmlift2lem6  35699  cvmlift2lem9  35702  cvmlift2lem11  35704  cvmlift2lem12  35705  mrsubvrs  35913  ellcsrspsn  36032  neibastop2lem  36760  topjoin  36765  fnejoin2  36769  weiunse  36868  pibt2  37951  lindsadd  38152  poimirlem3  38162  poimirlem9  38168  poimirlem28  38187  poimirlem32  38191  prdsbnd  38332  heiborlem8  38357  rrnequiv  38374  grpokerinj  38432  0idl  38564  prnc  38606  isfldidl  38607  lshpnel2N  39649  lsatfixedN  39673  lfl0f  39733  lkrlsp3  39768  elpaddatriN  40467  elpaddat  40468  elpadd2at  40470  pmodlem1  40510  osumcllem1N  40620  osumcllem2N  40621  osumcllem9N  40628  osumcllem10N  40629  pexmidlem6N  40639  pexmidlem7N  40640  dibss  41833  dochocsn  42045  dochsncom  42046  dochnel  42057  dihprrnlem1N  42088  dihprrnlem2  42089  djhlsmat  42091  dihsmsprn  42094  dvh4dimlem  42107  dvhdimlem  42108  dochsnnz  42114  dochsatshp  42115  dochsnshp  42117  dochexmid  42132  dochsnkr  42136  dochsnkr2cl  42138  dochfl1  42140  lcfl7lem  42163  lcfl6  42164  lcfl8  42166  lcfl9a  42169  lclkrlem2a  42171  lclkrlem2c  42173  lclkrlem2d  42174  lclkrlem2e  42175  lclkrlem2j  42180  lclkrlem2o  42185  lclkrlem2p  42186  lclkrlem2s  42189  lclkrlem2v  42192  lcfrlem14  42220  lcfrlem18  42224  lcfrlem19  42225  lcfrlem20  42226  lcfrlem23  42229  lcfrlem25  42231  lcdlkreqN  42286  mapdval4N  42296  mapdsn  42305  mapdhvmap  42433  hdmaprnlem4tN  42516  hdmapinvlem1  42582  hdmapinvlem2  42583  hdmapinvlem3  42584  hdmapinvlem4  42585  hdmapglem5  42586  hgmapvvlem3  42589  hdmapglem7a  42591  hdmapglem7b  42592  hdmapglem7  42593  hdmapoc  42595  aks6d1c5lem3  42794  deg1gprod  42797  sticksstones9  42811  sticksstones11  42813  rhmqusspan  42842  evlsbagval  43210  0prjspnrel  43251  elrfi  43317  cmpfiiin  43320  mzpcompact2lem  43374  dfac11  43681  pwssplit4  43708  rngunsnply  43788  flcidc  43789  proot1mul  43813  iocinico  43831  cantnfresb  43943  iunrelexp0  44320  frege81d  44365  k0004lem3  44767  mnuunid  44879  binomcxplemnn0  44951  islptre  46227  limciccioolb  46229  limcicciooub  46243  limcresiooub  46248  limcresioolb  46249  ioccncflimc  46491  icccncfext  46493  icocncflimc  46495  cncfiooicc  46500  dvnprodlem2  46553  dirkercncflem2  46710  dirkercncflem3  46711  fourierdlem48  46760  fourierdlem49  46761  fourierdlem79  46791  fourierdlem101  46813  sge0sup  46997  hoidmvlelem2  47202  hoiqssbl  47231  hspmbllem1  47232  hspmbllem2  47233  ovnovollem1  47262  fsumsplitsndif  48007  imaelsetpreimafv  48033  perfectALTVlem2  48376  stgrclnbgr0  48619  isubgr3stgrlem3  48622  1hegrlfgr  48786  gsumdifsndf  48835  sepfsepc  49591  discsubc  49727  iinfconstbas  49729