Theorem snssd 4747

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 4746	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-sn 4585

This theorem is used by:  intidg  5425  sofld  6179  fsnex  7291  fr3nr  7786  resf1extb  7946  resf1ext2b  7947  frrlem13  8316  oeeui  8611  naddunif  8703  naddasslem1  8704  naddasslem2  8705  ecinxp  8813  ralxpmap  8924  xpdom3  9094  domunsn  9146  mapdom3  9168  isinf  9256  ac6sfi  9275  pwfilem  9309  finsschain  9348  ssfii  9411  marypha1lem  9425  unxpwdom2  9582  en2other2  10088  fseqenlem1  10103  axdc3lem4  10531  axdc4lem  10533  ttukeylem7  10593  fpwwe2lem12  10727  canthwe  10736  canthp1lem1  10737  wuncval2  10832  un0addcl  12639  un0mulcl  12640  ssfzunsnext  13703  fseq1p1m1  13732  hashbclem  14597  hashf1lem1  14600  s1f1  14756  fsumsplit1  15911  fsumge1  15964  incexclem  16005  isumltss  16017  fprodsplit1f  16157  rpnnen2lem11  16392  bitsinv1  16612  lcmfunsnlem2  16815  lcmfass  16821  phicl2  16945  vdwlem1  17159  vdwlem8  17166  vdwlem12  17170  vdwlem13  17171  0ram  17198  ramub1lem1  17204  ramub1lem2  17205  ramcl  17207  imasaddfnlem  17700  imasaddflem  17702  imasvscafn  17709  imasvscaf  17711  mrieqvlemd  17803  mreexmrid  17817  mreexexlem4d  17821  acsfiindd  18727  acsmapd  18728  chnccat  18800  gsumress  18871  0subm  19013  gsumvallem2  19030  trivsubgd  19363  trivsubgsnd  19364  trivnsgd  19382  cycsubg2cl  19426  kerf1ghm  19461  pmtrprfv  19667  odf1o1  19786  gex1  19805  sylow2alem1  19831  sylow2alem2  19832  lsm01  19885  lsm02  19886  lsmdisj  19895  lsmdisj2  19896  prmcyg  20108  gsumzadd  20136  gsumconst  20148  gsumdifsnd  20175  gsumpt  20176  gsumxp  20190  dmdprdd  20215  dprdfadd  20236  dprdres  20244  dprdz  20246  dprdsn  20252  dprddisj2  20255  dprd2da  20258  dprd2d2  20260  dmdprdsplit2lem  20261  dpjcntz  20268  dpjdisj  20269  dpjlsm  20270  dpjidcl  20274  ablfacrp  20282  ablfac1eu  20289  pgpfac1lem1  20290  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfaclem2  20298  acsfn1p  21056  lsssn0  21223  lss0ss  21224  lsptpcl  21254  lspsnvsi  21279  lspun0  21286  pwssplit1  21334  lsmpr  21364  lsppr  21368  lspsntri  21372  lspsolvlem  21420  lspsolv  21421  lsppratlem1  21425  lsppratlem3  21427  lsppratlem4  21428  islbs3  21433  lbsextlem4  21439  rnglidl0  21509  0ringidl  21514  rsp1  21520  lidlnz  21530  drngidl  21539  isprmidlc  21628  qsidomlem2  21637  ssdifidlprm  21642  lidldvgen  21658  mulgrhm2  21784  zndvds  21855  psrlidm  22269  psrridm  22270  mplmonmul  22345  selvvvval  22451  mdetdiaglem  22913  mdetrlin  22917  mdetrsca  22918  mdetrsca2  22919  mdetrlin2  22922  mdetunilem5  22931  mdetunilem9  22935  mdetmul  22938  en2top  23303  rest0  23487  ordtrest  23520  iscnp4  23581  cnconst2  23601  cnpdis  23611  ist1-2  23665  cnt1  23668  dishaus  23700  discmp  23716  cmpcld  23720  conncompid  23749  dis2ndc  23779  dislly  23816  dissnref  23847  comppfsc  23851  llycmpkgen2  23869  cmpkgen  23870  1stckgenlem  23872  1stckgen  23873  ptbasfi  23900  txdis  23951  txdis1cn  23954  txcmplem1  23960  xkohaus  23972  xkoptsub  23973  xkoinjcn  24006  snfbas  24185  trnei  24211  isufil2  24227  ufileu  24238  filufint  24239  uffixsn  24244  ufildom1  24245  flimopn  24294  hausflim  24300  flimcf  24301  flimclslem  24303  flimsncls  24305  cnpflf2  24319  cnpflf  24320  fclsneii  24336  fclsfnflim  24346  fcfnei  24354  flfcntr  24362  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem2  24372  cldsubg  24430  snclseqg  24435  qustgphaus  24442  tsmsgsum  24458  tsmsid  24459  tgptsmscld  24470  tsmsxplem1  24472  tsmsxplem2  24473  ust0  24539  ustuqtop1  24560  neipcfilu  24614  prdsdsf  24686  prdsxmetlem  24687  prdsmet  24689  imasdsf1olem  24692  xpsdsval  24700  prdsbl  24810  prdsxmslem2  24848  idnghm  25062  icccmplem2  25143  metnrmlem2  25180  ioombl  25886  volivth  25928  itg11  26012  i1fmulclem  26023  itg2mulclem  26067  itgsplitioo  26158  limcvallem  26191  limcdif  26196  ellimc2  26197  limcflf  26201  limcmpt2  26204  limcres  26206  cnplimc  26207  limccnp  26211  limccnp2  26212  limcco  26213  dvreslem  26229  dvaddbr  26258  dvmulbr  26259  dvcmulf  26265  dvef  26300  dvivth  26330  lhop2  26335  lhop  26336  ply1remlem  26483  fta1blem  26489  ig1peu  26493  ig1pdvds  26498  plyco0  26510  elply2  26514  plyf  26516  elplyr  26519  elplyd  26520  ply1term  26522  ply0  26526  plyeq0lem  26529  plyeq0  26530  plypf1  26531  plyaddlem  26534  plymullem  26535  dgrlem  26548  coef2  26550  coeidlem  26556  plyco  26560  coemulhi  26573  plycj  26596  plyn0mulidp  26602  vieta1  26635  taylf  26688  radcnv0  26743  abelth  26768  rlimcnp  27293  xrlimcnp  27296  amgm  27318  wilthlem2  27396  basellem7  27414  basellem9  27416  ppiprm  27478  chtprm  27480  musumsum  27519  muinv  27520  logexprlim  27552  perfectlem2  27557  dchrhash  27598  rpvmasum2  27839  sltssnb  28155  conway  28165  lesrec  28185  eqcuts3  28190  cofcutr  28310  cutlt  28318  cutmax  28320  cutmin  28321  cutminmax  28322  addsuniflem  28387  negsunif  28441  sltmuls1  28533  sltmuls2  28534  precsexlem11  28603  oncutlt  28650  n0fincut  28741  bdaypw2n0bndlem  28849  axlowdimlem7  29526  axlowdimlem10  29529  upgrex  29670  upgr1elem  29690  uvtxnm1nbgr  29985  umgr2v2e  30106  pthhashvtx  30315  cyclnumvtx  30388  0oo  31391  sh0le  32042  disjiunel  33190  preimane  33263  fnpreimac  33264  fsuppinisegfi  33280  fprodeq02  33415  indsn  33430  gsumzresunsn  33623  gsumhashmul  33628  pmtrcnelor  33652  primefldgen1  33883  dvdsrspss  33942  elgrplsmsn  33945  lsmsnorb  33946  grplsm0l  33954  grplsmid  33955  unitpidl1  33974  elrspunsn  33979  mxidlprm  33995  mxidlirredi  33996  mxidlirred  33997  drngmxidl  34001  drngmxidlr  34002  qsdrngilem  34018  dflringlem  34026  rsprprmprmidl  34054  rprmirredb  34064  1arithufdlem4  34079  selvply1rhmlem1  34152  selvply1rhmlem2  34153  selvply1rhmlem4  34155  selvply1rhmlem5  34156  selvply1rhm  34157  selvply1rhm0  34158  mvrvalind  34170  mplmulmvr  34171  evlextv  34174  psrmonmul  34182  esplyfval0  34196  esplyfvaln  34206  esplyind  34207  esplyindfv  34208  vietalem  34211  lsatdim  34249  drngdimgt0  34250  dimkerim  34259  evls1fldgencl  34302  algextdeglem1  34349  algextdeglem2  34350  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  rtelextdg2  34359  constrextdg2lem  34380  constrext2chnlem  34382  constrfiss  34383  qtopt1  34467  locfinref  34473  zarcls0  34500  zarmxt1  34512  zarcmplem  34513  ordtrestNEW  34553  esumsnf  34696  esum2dlem  34724  rossros  34813  oms0  34929  carsggect  34950  eulerpartlems  34992  eulerpartlemgc  34994  eulerpartlemgh  35010  eulerpartlemgs2  35012  circlemeth  35269  hgt750lemb  35285  hgt750leme  35287  bnj1452  35682  subfacp1lem1  35944  subfacp1lem5  35949  erdszelem4  35959  erdszelem8  35963  sconnpi1  36004  cvmscld  36038  cvmlift2lem6  36073  cvmlift2lem9  36076  cvmlift2lem11  36078  cvmlift2lem12  36079  mrsubvrs  36287  ellcsrspsn  36406  neibastop2lem  37148  topjoin  37153  fnejoin2  37157  weiunse  37256  pibt2  38340  lindsadd  38536  poimirlem3  38541  poimirlem9  38547  poimirlem28  38566  poimirlem32  38570  prdsbnd  38727  heiborlem8  38752  rrnequiv  38769  grpokerinj  38827  0idl  38959  prnc  39001  isfldidl  39002  lshpnel2N  40042  lsatfixedN  40066  lfl0f  40126  lkrlsp3  40161  elpaddatriN  40860  elpaddat  40861  elpadd2at  40863  pmodlem1  40903  osumcllem1N  41013  osumcllem2N  41014  osumcllem9N  41021  osumcllem10N  41022  pexmidlem6N  41032  pexmidlem7N  41033  dibss  42226  dochocsn  42438  dochsncom  42439  dochnel  42450  dihprrnlem1N  42481  dihprrnlem2  42482  djhlsmat  42484  dihsmsprn  42487  dvh4dimlem  42500  dvhdimlem  42501  dochsnnz  42507  dochsatshp  42508  dochsnshp  42510  dochexmid  42525  dochsnkr  42529  dochsnkr2cl  42531  dochfl1  42533  lcfl7lem  42556  lcfl6  42557  lcfl8  42559  lcfl9a  42562  lclkrlem2a  42564  lclkrlem2c  42566  lclkrlem2d  42567  lclkrlem2e  42568  lclkrlem2j  42573  lclkrlem2o  42578  lclkrlem2p  42579  lclkrlem2s  42582  lclkrlem2v  42585  lcfrlem14  42613  lcfrlem18  42617  lcfrlem19  42618  lcfrlem20  42619  lcfrlem23  42622  lcfrlem25  42624  lcdlkreqN  42679  mapdval4N  42689  mapdsn  42698  mapdhvmap  42826  hdmaprnlem4tN  42909  hdmapinvlem1  42975  hdmapinvlem2  42976  hdmapinvlem3  42977  hdmapinvlem4  42978  hdmapglem5  42979  hgmapvvlem3  42982  hdmapglem7a  42984  hdmapglem7b  42985  hdmapglem7  42986  hdmapoc  42988  aks6d1c5lem3  43187  deg1gprod  43190  sticksstones9  43204  sticksstones11  43206  rhmqusspan  43235  evlsbagval  43614  0prjspnrel  43663  elrfi  43704  cmpfiiin  43707  mzpcompact2lem  43761  dfac11  44063  pwssplit4  44090  rngunsnply  44170  flcidc  44171  proot1mul  44195  iocinico  44213  cantnfresb  44325  iunrelexp0  44701  frege81d  44746  k0004lem3  45148  mnuunid  45260  binomcxplemnn0  45332  islptre  46630  limciccioolb  46632  limcicciooub  46646  limcresiooub  46651  limcresioolb  46652  ioccncflimc  46894  icccncfext  46896  icocncflimc  46898  cncfiooicc  46903  dvnprodlem2  46956  dirkercncflem2  47113  dirkercncflem3  47114  fourierdlem48  47163  fourierdlem49  47164  fourierdlem79  47194  fourierdlem101  47216  sge0sup  47400  hoidmvlelem2  47605  hoiqssbl  47634  hspmbllem1  47635  hspmbllem2  47636  ovnovollem1  47665  tmachlem-agreeprod  47946  tmachlem-agreesn  47956  fsumsplitsndif  48450  imaelsetpreimafv  48476  perfectALTVlem2  48819  stgrclnbgr0  49062  isubgr3stgrlem3  49065  1hegrlfgr  49229  gsumdifsndf  49277  sepfsepc  50035  discsubc  50171  iinfconstbas  50173