Theorem snssd 4718

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-sn 4556

This theorem is referenced by:  intidg  5396  sofld  6138  fsnex  7227  fr3nr  7715  resf1extb  7874  resf1ext2b  7875  frrlem13  8238  oeeui  8528  naddunif  8619  naddasslem1  8620  naddasslem2  8621  ecinxp  8729  ralxpmap  8834  xpdom3  9003  domunsn  9055  mapdom3  9077  isinf  9165  ac6sfi  9184  pwfilem  9218  finsschain  9259  ssfii  9322  marypha1lem  9336  unxpwdom2  9493  en2other2  9922  fseqenlem1  9937  axdc3lem4  10366  axdc4lem  10368  ttukeylem7  10428  fpwwe2lem12  10556  canthwe  10565  canthp1lem1  10566  wuncval2  10661  un0addcl  12461  un0mulcl  12462  ssfzunsnext  13514  fseq1p1m1  13543  hashbclem  14405  hashf1lem1  14408  fsumsplit1  15698  fsumge1  15751  incexclem  15792  isumltss  15804  fprodsplit1f  15946  rpnnen2lem11  16182  bitsinv1  16402  lcmfunsnlem2  16600  lcmfass  16606  phicl2  16729  vdwlem1  16943  vdwlem8  16950  vdwlem12  16954  vdwlem13  16955  0ram  16982  ramub1lem1  16988  ramub1lem2  16989  ramcl  16991  imasaddfnlem  17483  imasaddflem  17485  imasvscafn  17492  imasvscaf  17494  mrieqvlemd  17586  mreexmrid  17600  mreexexlem4d  17604  acsfiindd  18510  acsmapd  18511  chnccat  18583  gsumress  18641  0subm  18776  gsumvallem2  18793  trivsubgd  19119  trivsubgsnd  19120  trivnsgd  19138  cycsubg2cl  19177  kerf1ghm  19213  pmtrprfv  19419  odf1o1  19538  gex1  19557  sylow2alem1  19583  sylow2alem2  19584  lsm01  19637  lsm02  19638  lsmdisj  19647  lsmdisj2  19648  prmcyg  19860  gsumzadd  19888  gsumconst  19900  gsumdifsnd  19927  gsumpt  19928  gsumxp  19942  dmdprdd  19967  dprdfadd  19988  dprdres  19996  dprdz  19998  dprdsn  20004  dprddisj2  20007  dprd2da  20010  dprd2d2  20012  dmdprdsplit2lem  20013  dpjcntz  20020  dpjdisj  20021  dpjlsm  20022  dpjidcl  20026  ablfacrp  20034  ablfac1eu  20041  pgpfac1lem1  20042  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfaclem2  20050  acsfn1p  20771  lsssn0  20938  lss0ss  20939  lsptpcl  20969  lspsnvsi  20994  lspun0  21001  pwssplit1  21049  lsmpr  21079  lsppr  21083  lspsntri  21087  lspsolvlem  21135  lspsolv  21136  lsppratlem1  21140  lsppratlem3  21142  lsppratlem4  21143  islbs3  21148  lbsextlem4  21154  rnglidl0  21222  rsp1  21230  lidlnz  21235  lidldvgen  21327  mulgrhm2  21453  zndvds  21524  psrlidm  21936  psrridm  21937  mplmonmul  22012  selvvvval  22118  mdetdiaglem  22581  mdetrlin  22585  mdetrsca  22586  mdetrsca2  22587  mdetrlin2  22590  mdetunilem5  22599  mdetunilem9  22603  mdetmul  22606  en2top  22968  rest0  23152  ordtrest  23185  iscnp4  23246  cnconst2  23266  cnpdis  23276  ist1-2  23330  cnt1  23333  dishaus  23365  discmp  23381  cmpcld  23385  conncompid  23414  dis2ndc  23443  dislly  23480  dissnref  23511  comppfsc  23515  llycmpkgen2  23533  cmpkgen  23534  1stckgenlem  23536  1stckgen  23537  ptbasfi  23564  txdis  23615  txdis1cn  23618  txcmplem1  23624  xkohaus  23636  xkoptsub  23637  xkoinjcn  23670  snfbas  23849  trnei  23875  isufil2  23891  ufileu  23902  filufint  23903  uffixsn  23908  ufildom1  23909  flimopn  23958  hausflim  23964  flimcf  23965  flimclslem  23967  flimsncls  23969  cnpflf2  23983  cnpflf  23984  fclsneii  24000  fclsfnflim  24010  fcfnei  24018  flfcntr  24026  alexsubALTlem3  24032  alexsubALTlem4  24033  ptcmplem2  24036  cldsubg  24094  snclseqg  24099  qustgphaus  24106  tsmsgsum  24122  tsmsid  24123  tgptsmscld  24134  tsmsxplem1  24136  tsmsxplem2  24137  ust0  24203  ustuqtop1  24224  neipcfilu  24278  prdsdsf  24350  prdsxmetlem  24351  prdsmet  24353  imasdsf1olem  24356  xpsdsval  24364  prdsbl  24474  prdsxmslem2  24512  idnghm  24726  icccmplem2  24807  metnrmlem2  24844  ioombl  25550  volivth  25592  itg11  25676  i1fmulclem  25687  itg2mulclem  25731  itgsplitioo  25823  limcvallem  25856  limcdif  25861  ellimc2  25862  limcflf  25866  limcmpt2  25869  limcres  25871  cnplimc  25872  limccnp  25876  limccnp2  25877  limcco  25878  dvreslem  25894  dvaddbr  25923  dvmulbr  25924  dvcmulf  25930  dvef  25965  dvivth  25995  lhop2  26000  lhop  26001  ply1remlem  26148  fta1blem  26154  ig1peu  26158  ig1pdvds  26163  plyco0  26175  elply2  26179  plyf  26181  elplyr  26184  elplyd  26185  ply1term  26187  ply0  26191  plyeq0lem  26193  plyeq0  26194  plypf1  26195  plyaddlem  26198  plymullem  26199  dgrlem  26212  coef2  26214  coeidlem  26220  plyco  26224  coemulhi  26237  plycj  26260  plycjOLD  26262  vieta1  26296  taylf  26344  radcnv0  26399  abelth  26424  rlimcnp  26947  xrlimcnp  26950  amgm  26972  wilthlem2  27050  basellem7  27068  basellem9  27070  ppiprm  27132  chtprm  27134  musumsum  27173  muinv  27174  logexprlim  27206  perfectlem2  27211  dchrhash  27252  rpvmasum2  27493  sltssnb  27779  conway  27789  lesrec  27809  eqcuts3  27814  cofcutr  27934  cutlt  27942  cutmax  27944  cutmin  27945  cutminmax  27946  addsuniflem  28011  negsunif  28065  sltmuls1  28157  sltmuls2  28158  precsexlem11  28227  oncutlt  28274  n0fincut  28365  bdaypw2n0bndlem  28473  axlowdimlem7  29035  axlowdimlem10  29038  upgrex  29179  upgr1elem  29199  uvtxnm1nbgr  29491  umgr2v2e  29612  cyclnumvtx  29886  0oo  30878  sh0le  31529  disjiunel  32685  preimane  32761  fnpreimac  32762  fsuppinisegfi  32779  fprodeq02  32916  indsn  32942  s1f1  33022  gsumzresunsn  33143  gsumhashmul  33148  pmtrcnelor  33172  primefldgen1  33405  dvdsrspss  33470  elgrplsmsn  33473  lsmsnorb  33474  grplsm0l  33486  grplsmid  33487  0ringidl  33504  unitpidl1  33507  elrspunsn  33512  drngidl  33516  isprmidlc  33530  qsidomlem2  33536  ssdifidlprm  33541  mxidlprm  33553  mxidlirredi  33554  mxidlirred  33555  drngmxidl  33560  drngmxidlr  33561  qsdrngilem  33577  rsprprmprmidl  33605  rprmirredb  33615  1arithufdlem4  33630  selvply1rhmlem1  33704  selvply1rhmlem2  33705  selvply1rhmlem4  33707  selvply1rhmlem5  33708  selvply1rhm  33709  selvply1rhm0  33710  mvrvalind  33722  mplmulmvr  33723  evlextv  33726  psrmonmul  33734  esplyfval0  33748  esplyfvaln  33758  esplyind  33759  esplyindfv  33760  vietalem  33763  lsatdim  33801  drngdimgt0  33802  dimkerim  33811  evls1fldgencl  33854  algextdeglem1  33901  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  rtelextdg2  33911  constrextdg2lem  33932  constrext2chnlem  33934  constrfiss  33935  qtopt1  34019  locfinref  34025  zarcls0  34052  zarmxt1  34064  zarcmplem  34065  ordtrestNEW  34105  esumsnf  34248  esum2dlem  34276  rossros  34364  oms0  34481  carsggect  34502  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemgh  34562  eulerpartlemgs2  34564  plymulx0  34731  circlemeth  34824  hgt750lemb  34840  hgt750leme  34842  bnj1452  35234  pthhashvtx  35356  subfacp1lem1  35407  subfacp1lem5  35412  erdszelem4  35422  erdszelem8  35426  sconnpi1  35467  cvmscld  35501  cvmlift2lem6  35536  cvmlift2lem9  35539  cvmlift2lem11  35541  cvmlift2lem12  35542  mrsubvrs  35750  ellcsrspsn  35869  neibastop2lem  36588  topjoin  36593  fnejoin2  36597  weiunse  36696  pibt2  37779  lindsadd  37980  poimirlem3  37990  poimirlem9  37996  poimirlem28  38015  poimirlem32  38019  prdsbnd  38160  heiborlem8  38185  rrnequiv  38202  grpokerinj  38260  0idl  38392  prnc  38434  isfldidl  38435  lshpnel2N  39477  lsatfixedN  39501  lfl0f  39561  lkrlsp3  39596  elpaddatriN  40295  elpaddat  40296  elpadd2at  40298  pmodlem1  40338  osumcllem1N  40448  osumcllem2N  40449  osumcllem9N  40456  osumcllem10N  40457  pexmidlem6N  40467  pexmidlem7N  40468  dibss  41661  dochocsn  41873  dochsncom  41874  dochnel  41885  dihprrnlem1N  41916  dihprrnlem2  41917  djhlsmat  41919  dihsmsprn  41922  dvh4dimlem  41935  dvhdimlem  41936  dochsnnz  41942  dochsatshp  41943  dochsnshp  41945  dochexmid  41960  dochsnkr  41964  dochsnkr2cl  41966  dochfl1  41968  lcfl7lem  41991  lcfl6  41992  lcfl8  41994  lcfl9a  41997  lclkrlem2a  41999  lclkrlem2c  42001  lclkrlem2d  42002  lclkrlem2e  42003  lclkrlem2j  42008  lclkrlem2o  42013  lclkrlem2p  42014  lclkrlem2s  42017  lclkrlem2v  42020  lcfrlem14  42048  lcfrlem18  42052  lcfrlem19  42053  lcfrlem20  42054  lcfrlem23  42057  lcfrlem25  42059  lcdlkreqN  42114  mapdval4N  42124  mapdsn  42133  mapdhvmap  42261  hdmaprnlem4tN  42344  hdmapinvlem1  42410  hdmapinvlem2  42411  hdmapinvlem3  42412  hdmapinvlem4  42413  hdmapglem5  42414  hgmapvvlem3  42417  hdmapglem7a  42419  hdmapglem7b  42420  hdmapglem7  42421  hdmapoc  42423  aks6d1c5lem3  42622  deg1gprod  42625  sticksstones9  42639  sticksstones11  42641  rhmqusspan  42670  evlsbagval  43036  0prjspnrel  43077  elrfi  43143  cmpfiiin  43146  mzpcompact2lem  43200  dfac11  43507  pwssplit4  43534  rngunsnply  43614  flcidc  43615  proot1mul  43639  iocinico  43657  cantnfresb  43769  iunrelexp0  44146  frege81d  44191  k0004lem3  44593  mnuunid  44721  binomcxplemnn0  44793  islptre  46064  limciccioolb  46066  limcicciooub  46080  limcresiooub  46085  limcresioolb  46086  ioccncflimc  46328  icccncfext  46330  icocncflimc  46332  cncfiooicc  46337  dvnprodlem2  46390  dirkercncflem2  46547  dirkercncflem3  46548  fourierdlem48  46597  fourierdlem49  46598  fourierdlem79  46628  fourierdlem101  46650  sge0sup  46834  hoidmvlelem2  47039  hoiqssbl  47068  hspmbllem1  47069  hspmbllem2  47070  ovnovollem1  47099  fsumsplitsndif  47844  imaelsetpreimafv  47870  perfectALTVlem2  48213  stgrclnbgr0  48456  isubgr3stgrlem3  48459  1hegrlfgr  48623  gsumdifsndf  48672  sepfsepc  49418  discsubc  49554  iinfconstbas  49556