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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-sn 4585

This theorem is used by:  intidg  5432  sofld  6180  fsnex  7285  fr3nr  7772  resf1extb  7932  resf1ext2b  7933  frrlem13  8298  oeeui  8591  naddunif  8683  naddasslem1  8684  naddasslem2  8685  ecinxp  8793  ralxpmap  8904  xpdom3  9074  domunsn  9126  mapdom3  9148  isinf  9236  ac6sfi  9255  pwfilem  9288  finsschain  9327  ssfii  9390  marypha1lem  9404  unxpwdom2  9561  en2other2  10013  fseqenlem1  10028  axdc3lem4  10456  axdc4lem  10458  ttukeylem7  10518  fpwwe2lem12  10652  canthwe  10661  canthp1lem1  10662  wuncval2  10757  un0addcl  12562  un0mulcl  12563  ssfzunsnext  13625  fseq1p1m1  13654  hashbclem  14518  hashf1lem1  14521  s1f1  14677  fsumsplit1  15832  fsumge1  15885  incexclem  15926  isumltss  15938  fprodsplit1f  16078  rpnnen2lem11  16313  bitsinv1  16533  lcmfunsnlem2  16731  lcmfass  16737  phicl2  16860  vdwlem1  17074  vdwlem8  17081  vdwlem12  17085  vdwlem13  17086  0ram  17113  ramub1lem1  17119  ramub1lem2  17120  ramcl  17122  imasaddfnlem  17615  imasaddflem  17617  imasvscafn  17624  imasvscaf  17626  mrieqvlemd  17718  mreexmrid  17732  mreexexlem4d  17736  acsfiindd  18642  acsmapd  18643  chnccat  18715  gsumress  18785  0subm  18927  gsumvallem2  18944  trivsubgd  19277  trivsubgsnd  19278  trivnsgd  19296  cycsubg2cl  19340  kerf1ghm  19375  pmtrprfv  19581  odf1o1  19700  gex1  19719  sylow2alem1  19745  sylow2alem2  19746  lsm01  19799  lsm02  19800  lsmdisj  19809  lsmdisj2  19810  prmcyg  20022  gsumzadd  20050  gsumconst  20062  gsumdifsnd  20089  gsumpt  20090  gsumxp  20104  dmdprdd  20129  dprdfadd  20150  dprdres  20158  dprdz  20160  dprdsn  20166  dprddisj2  20169  dprd2da  20172  dprd2d2  20174  dmdprdsplit2lem  20175  dpjcntz  20182  dpjdisj  20183  dpjlsm  20184  dpjidcl  20188  ablfacrp  20196  ablfac1eu  20203  pgpfac1lem1  20204  pgpfac1lem3a  20206  pgpfac1lem3  20207  pgpfac1lem5  20209  pgpfaclem2  20212  acsfn1p  20966  lsssn0  21133  lss0ss  21134  lsptpcl  21164  lspsnvsi  21189  lspun0  21196  pwssplit1  21244  lsmpr  21274  lsppr  21278  lspsntri  21282  lspsolvlem  21330  lspsolv  21331  lsppratlem1  21335  lsppratlem3  21337  lsppratlem4  21338  islbs3  21343  lbsextlem4  21349  rnglidl0  21419  0ringidl  21424  rsp1  21430  lidlnz  21440  drngidl  21449  isprmidlc  21536  qsidomlem2  21545  ssdifidlprm  21550  lidldvgen  21566  mulgrhm2  21692  zndvds  21763  psrlidm  22177  psrridm  22178  mplmonmul  22253  selvvvval  22359  mdetdiaglem  22821  mdetrlin  22825  mdetrsca  22826  mdetrsca2  22827  mdetrlin2  22830  mdetunilem5  22839  mdetunilem9  22843  mdetmul  22846  en2top  23211  rest0  23395  ordtrest  23428  iscnp4  23489  cnconst2  23509  cnpdis  23519  ist1-2  23573  cnt1  23576  dishaus  23608  discmp  23624  cmpcld  23628  conncompid  23657  dis2ndc  23687  dislly  23724  dissnref  23755  comppfsc  23759  llycmpkgen2  23777  cmpkgen  23778  1stckgenlem  23780  1stckgen  23781  ptbasfi  23808  txdis  23859  txdis1cn  23862  txcmplem1  23868  xkohaus  23880  xkoptsub  23881  xkoinjcn  23914  snfbas  24093  trnei  24119  isufil2  24135  ufileu  24146  filufint  24147  uffixsn  24152  ufildom1  24153  flimopn  24202  hausflim  24208  flimcf  24209  flimclslem  24211  flimsncls  24213  cnpflf2  24227  cnpflf  24228  fclsneii  24244  fclsfnflim  24254  fcfnei  24262  flfcntr  24270  alexsubALTlem3  24276  alexsubALTlem4  24277  ptcmplem2  24280  cldsubg  24338  snclseqg  24343  qustgphaus  24350  tsmsgsum  24366  tsmsid  24367  tgptsmscld  24378  tsmsxplem1  24380  tsmsxplem2  24381  ust0  24447  ustuqtop1  24468  neipcfilu  24522  prdsdsf  24594  prdsxmetlem  24595  prdsmet  24597  imasdsf1olem  24600  xpsdsval  24608  prdsbl  24718  prdsxmslem2  24756  idnghm  24970  icccmplem2  25051  metnrmlem2  25088  ioombl  25794  volivth  25836  itg11  25920  i1fmulclem  25931  itg2mulclem  25975  itgsplitioo  26066  limcvallem  26099  limcdif  26104  ellimc2  26105  limcflf  26109  limcmpt2  26112  limcres  26114  cnplimc  26115  limccnp  26119  limccnp2  26120  limcco  26121  dvreslem  26137  dvaddbr  26166  dvmulbr  26167  dvcmulf  26173  dvef  26208  dvivth  26238  lhop2  26243  lhop  26244  ply1remlem  26391  fta1blem  26397  ig1peu  26401  ig1pdvds  26406  plyco0  26418  elply2  26422  plyf  26424  elplyr  26427  elplyd  26428  ply1term  26430  ply0  26434  plyeq0lem  26437  plyeq0  26438  plypf1  26439  plyaddlem  26442  plymullem  26443  dgrlem  26456  coef2  26458  coeidlem  26464  plyco  26468  coemulhi  26481  plycj  26504  plycjOLD  26506  plyn0mulidp  26512  vieta1  26545  taylf  26598  radcnv0  26653  abelth  26678  rlimcnp  27203  xrlimcnp  27206  amgm  27228  wilthlem2  27306  basellem7  27324  basellem9  27326  ppiprm  27388  chtprm  27390  musumsum  27429  muinv  27430  logexprlim  27462  perfectlem2  27467  dchrhash  27508  rpvmasum2  27749  sltssnb  28035  conway  28045  lesrec  28065  eqcuts3  28070  cofcutr  28190  cutlt  28198  cutmax  28200  cutmin  28201  cutminmax  28202  addsuniflem  28267  negsunif  28321  sltmuls1  28413  sltmuls2  28414  precsexlem11  28483  oncutlt  28530  n0fincut  28621  bdaypw2n0bndlem  28729  axlowdimlem7  29406  axlowdimlem10  29409  upgrex  29550  upgr1elem  29570  uvtxnm1nbgr  29865  umgr2v2e  29986  pthhashvtx  30195  cyclnumvtx  30268  0oo  31271  sh0le  31922  disjiunel  33070  preimane  33143  fnpreimac  33144  fsuppinisegfi  33160  fprodeq02  33295  indsn  33310  gsumzresunsn  33503  gsumhashmul  33508  pmtrcnelor  33532  primefldgen1  33763  dvdsrspss  33821  elgrplsmsn  33824  lsmsnorb  33825  grplsm0l  33833  grplsmid  33834  unitpidl1  33853  elrspunsn  33858  mxidlprm  33874  mxidlirredi  33875  mxidlirred  33876  drngmxidl  33880  drngmxidlr  33881  qsdrngilem  33897  dflringlem  33905  rsprprmprmidl  33933  rprmirredb  33943  1arithufdlem4  33958  selvply1rhmlem1  34031  selvply1rhmlem2  34032  selvply1rhmlem4  34034  selvply1rhmlem5  34035  selvply1rhm  34036  selvply1rhm0  34037  mvrvalind  34049  mplmulmvr  34050  evlextv  34053  psrmonmul  34061  esplyfval0  34075  esplyfvaln  34085  esplyind  34086  esplyindfv  34087  vietalem  34090  lsatdim  34128  drngdimgt0  34129  dimkerim  34138  evls1fldgencl  34181  algextdeglem1  34228  algextdeglem2  34229  algextdeglem3  34230  algextdeglem4  34231  algextdeglem5  34232  rtelextdg2  34238  constrextdg2lem  34259  constrext2chnlem  34261  constrfiss  34262  qtopt1  34346  locfinref  34352  zarcls0  34379  zarmxt1  34391  zarcmplem  34392  ordtrestNEW  34432  esumsnf  34575  esum2dlem  34603  rossros  34692  oms0  34809  carsggect  34830  eulerpartlems  34872  eulerpartlemgc  34874  eulerpartlemgh  34890  eulerpartlemgs2  34892  circlemeth  35149  hgt750lemb  35165  hgt750leme  35167  bnj1452  35562  subfacp1lem1  35759  subfacp1lem5  35764  erdszelem4  35774  erdszelem8  35778  sconnpi1  35819  cvmscld  35853  cvmlift2lem6  35888  cvmlift2lem9  35891  cvmlift2lem11  35893  cvmlift2lem12  35894  mrsubvrs  36102  ellcsrspsn  36221  neibastop2lem  36980  topjoin  36985  fnejoin2  36989  weiunse  37088  pibt2  38172  lindsadd  38368  poimirlem3  38373  poimirlem9  38379  poimirlem28  38398  poimirlem32  38402  prdsbnd  38544  heiborlem8  38569  rrnequiv  38586  grpokerinj  38644  0idl  38776  prnc  38818  isfldidl  38819  lshpnel2N  39859  lsatfixedN  39883  lfl0f  39943  lkrlsp3  39978  elpaddatriN  40677  elpaddat  40678  elpadd2at  40680  pmodlem1  40720  osumcllem1N  40830  osumcllem2N  40831  osumcllem9N  40838  osumcllem10N  40839  pexmidlem6N  40849  pexmidlem7N  40850  dibss  42043  dochocsn  42255  dochsncom  42256  dochnel  42267  dihprrnlem1N  42298  dihprrnlem2  42299  djhlsmat  42301  dihsmsprn  42304  dvh4dimlem  42317  dvhdimlem  42318  dochsnnz  42324  dochsatshp  42325  dochsnshp  42327  dochexmid  42342  dochsnkr  42346  dochsnkr2cl  42348  dochfl1  42350  lcfl7lem  42373  lcfl6  42374  lcfl8  42376  lcfl9a  42379  lclkrlem2a  42381  lclkrlem2c  42383  lclkrlem2d  42384  lclkrlem2e  42385  lclkrlem2j  42390  lclkrlem2o  42395  lclkrlem2p  42396  lclkrlem2s  42399  lclkrlem2v  42402  lcfrlem14  42430  lcfrlem18  42434  lcfrlem19  42435  lcfrlem20  42436  lcfrlem23  42439  lcfrlem25  42441  lcdlkreqN  42496  mapdval4N  42506  mapdsn  42515  mapdhvmap  42643  hdmaprnlem4tN  42726  hdmapinvlem1  42792  hdmapinvlem2  42793  hdmapinvlem3  42794  hdmapinvlem4  42795  hdmapglem5  42796  hgmapvvlem3  42799  hdmapglem7a  42801  hdmapglem7b  42802  hdmapglem7  42803  hdmapoc  42805  aks6d1c5lem3  43004  deg1gprod  43007  sticksstones9  43021  sticksstones11  43023  rhmqusspan  43052  evlsbagval  43433  0prjspnrel  43474  elrfi  43540  cmpfiiin  43543  mzpcompact2lem  43597  dfac11  43904  pwssplit4  43931  rngunsnply  44011  flcidc  44012  proot1mul  44036  iocinico  44054  cantnfresb  44166  iunrelexp0  44543  frege81d  44588  k0004lem3  44990  mnuunid  45102  binomcxplemnn0  45174  islptre  46450  limciccioolb  46452  limcicciooub  46466  limcresiooub  46471  limcresioolb  46472  ioccncflimc  46714  icccncfext  46716  icocncflimc  46718  cncfiooicc  46723  dvnprodlem2  46776  dirkercncflem2  46933  dirkercncflem3  46934  fourierdlem48  46983  fourierdlem49  46984  fourierdlem79  47014  fourierdlem101  47036  sge0sup  47220  hoidmvlelem2  47425  hoiqssbl  47454  hspmbllem1  47455  hspmbllem2  47456  ovnovollem1  47485  tmachlem-agreeprod  47766  tmachlem-agreesn  47776  fsumsplitsndif  48270  imaelsetpreimafv  48296  perfectALTVlem2  48639  stgrclnbgr0  48882  isubgr3stgrlem3  48885  1hegrlfgr  49049  gsumdifsndf  49097  sepfsepc  49855  discsubc  49991  iinfconstbas  49993