Theorem snssd 4746

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-sn 4588

This theorem is used by:  intidg  5428  sofld  6184  fsnex  7298  fr3nr  7793  resf1extb  7953  resf1ext2b  7954  frrlem13  8327  oeeui  8622  naddunif  8714  naddasslem1  8715  naddasslem2  8716  ecinxp  8824  ralxpmap  8935  xpdom3  9105  domunsn  9157  mapdom3  9179  isinf  9267  ac6sfi  9286  pwfilem  9320  finsschain  9359  ssfii  9421  marypha1lem  9435  unxpwdom2  9592  en2other2  10098  fseqenlem1  10113  axdc3lem4  10541  axdc4lem  10543  ttukeylem7  10603  fpwwe2lem12  10737  canthwe  10746  canthp1lem1  10747  wuncval2  10842  un0addcl  12649  un0mulcl  12650  ssfzunsnext  13713  fseq1p1m1  13742  hashbclem  14607  hashf1lem1  14610  s1f1  14767  fsumsplit1  15923  fsumge1  15976  incexclem  16017  isumltss  16029  fprodsplit1f  16169  rpnnen2lem11  16404  bitsinv1  16624  lcmfunsnlem2  16827  lcmfass  16833  phicl2  16957  vdwlem1  17171  vdwlem8  17178  vdwlem12  17182  vdwlem13  17183  0ram  17210  ramub1lem1  17216  ramub1lem2  17217  ramcl  17219  imasaddfnlem  17712  imasaddflem  17714  imasvscafn  17721  imasvscaf  17723  mrieqvlemd  17815  mreexmrid  17829  mreexexlem4d  17833  acsfiindd  18739  acsmapd  18740  chnccat  18812  gsumress  18883  0subm  19025  gsumvallem2  19042  trivsubgd  19375  trivsubgsnd  19376  trivnsgd  19394  cycsubg2cl  19438  kerf1ghm  19473  pmtrprfv  19679  odf1o1  19798  gex1  19817  sylow2alem1  19843  sylow2alem2  19844  lsm01  19897  lsm02  19898  lsmdisj  19907  lsmdisj2  19908  prmcyg  20120  gsumzadd  20148  gsumconst  20160  gsumdifsnd  20187  gsumpt  20188  gsumxp  20202  dmdprdd  20227  dprdfadd  20248  dprdres  20256  dprdz  20258  dprdsn  20264  dprddisj2  20267  dprd2da  20270  dprd2d2  20272  dmdprdsplit2lem  20273  dpjcntz  20280  dpjdisj  20281  dpjlsm  20282  dpjidcl  20286  ablfacrp  20294  ablfac1eu  20301  pgpfac1lem1  20302  pgpfac1lem3a  20304  pgpfac1lem3  20305  pgpfac1lem5  20307  pgpfaclem2  20310  acsfn1p  21068  lsssn0  21235  lss0ss  21236  lsptpcl  21266  lspsnvsi  21291  lspun0  21298  pwssplit1  21346  lsmpr  21376  lsppr  21380  lspsntri  21384  lspsolvlem  21432  lspsolv  21433  lsppratlem1  21437  lsppratlem3  21439  lsppratlem4  21440  islbs3  21445  lbsextlem4  21451  rnglidl0  21521  0ringidl  21526  rsp1  21532  lidlnz  21542  drngidl  21551  isprmidlc  21640  qsidomlem2  21649  ssdifidlprm  21654  lidldvgen  21670  mulgrhm2  21796  zndvds  21867  psrlidm  22281  psrridm  22282  mplmonmul  22357  selvvvval  22463  mdetdiaglem  22925  mdetrlin  22929  mdetrsca  22930  mdetrsca2  22931  mdetrlin2  22934  mdetunilem5  22943  mdetunilem9  22947  mdetmul  22950  en2top  23315  rest0  23499  ordtrest  23532  iscnp4  23593  cnconst2  23613  cnpdis  23623  ist1-2  23677  cnt1  23680  dishaus  23712  discmp  23728  cmpcld  23732  conncompid  23761  dis2ndc  23791  dislly  23828  dissnref  23859  comppfsc  23863  llycmpkgen2  23881  cmpkgen  23882  1stckgenlem  23884  1stckgen  23885  ptbasfi  23912  txdis  23963  txdis1cn  23966  txcmplem1  23972  xkohaus  23984  xkoptsub  23985  xkoinjcn  24018  snfbas  24197  trnei  24223  isufil2  24239  ufileu  24250  filufint  24251  uffixsn  24256  ufildom1  24257  flimopn  24306  hausflim  24312  flimcf  24313  flimclslem  24315  flimsncls  24317  cnpflf2  24331  cnpflf  24332  fclsneii  24348  fclsfnflim  24358  fcfnei  24366  flfcntr  24374  alexsubALTlem3  24380  alexsubALTlem4  24381  ptcmplem2  24384  cldsubg  24442  snclseqg  24447  qustgphaus  24454  tsmsgsum  24470  tsmsid  24471  tgptsmscld  24482  tsmsxplem1  24484  tsmsxplem2  24485  ust0  24551  ustuqtop1  24572  neipcfilu  24626  prdsdsf  24698  prdsxmetlem  24699  prdsmet  24701  imasdsf1olem  24704  xpsdsval  24712  prdsbl  24822  prdsxmslem2  24860  idnghm  25074  icccmplem2  25155  metnrmlem2  25192  ioombl  25898  volivth  25940  itg11  26024  i1fmulclem  26035  itg2mulclem  26079  itgsplitioo  26170  limcvallem  26203  limcdif  26208  ellimc2  26209  limcflf  26213  limcmpt2  26216  limcres  26218  cnplimc  26219  limccnp  26223  limccnp2  26224  limcco  26225  dvreslem  26241  dvaddbr  26270  dvmulbr  26271  dvcmulf  26277  dvef  26312  dvivth  26342  lhop2  26347  lhop  26348  ply1remlem  26495  fta1blem  26501  ig1peu  26505  ig1pdvds  26510  plyco0  26522  elply2  26526  plyf  26528  elplyr  26531  elplyd  26532  ply1term  26534  ply0  26538  plyeq0lem  26541  plyeq0  26542  plypf1  26543  plyaddlem  26546  plymullem  26547  dgrlem  26560  coef2  26562  coeidlem  26568  plyco  26572  coemulhi  26585  plycj  26608  plyn0mulidp  26614  vieta1  26647  taylf  26700  radcnv0  26755  abelth  26780  rlimcnp  27305  xrlimcnp  27308  amgm  27330  wilthlem2  27408  basellem7  27426  basellem9  27428  ppiprm  27490  chtprm  27492  musumsum  27531  muinv  27532  logexprlim  27564  perfectlem2  27569  dchrhash  27610  rpvmasum2  27851  sltssnb  28167  conway  28177  lesrec  28197  eqcuts3  28202  cofcutr  28322  cutlt  28330  cutmax  28332  cutmin  28333  cutminmax  28334  addsuniflem  28399  negsunif  28453  sltmuls1  28545  sltmuls2  28546  precsexlem11  28615  oncutlt  28662  n0fincut  28753  bdaypw2n0bndlem  28861  axlowdimlem7  29538  axlowdimlem10  29541  upgrex  29682  upgr1elem  29702  uvtxnm1nbgr  29997  umgr2v2e  30118  pthhashvtx  30327  cyclnumvtx  30400  0oo  31403  sh0le  32054  disjiunel  33244  preimane  33317  fnpreimac  33318  fsuppinisegfi  33334  fprodeq02  33468  indsn  33483  gsumzresunsn  33676  gsumhashmul  33681  pmtrcnelor  33705  primefldgen1  33936  dvdsrspss  33995  elgrplsmsn  33998  lsmsnorb  33999  grplsm0l  34007  grplsmid  34008  unitpidl1  34027  elrspunsn  34032  mxidlprm  34048  mxidlirredi  34049  mxidlirred  34050  drngmxidl  34054  drngmxidlr  34055  qsdrngilem  34071  dflringlem  34079  rsprprmprmidl  34107  rprmirredb  34117  1arithufdlem4  34132  selvply1rhmlem1  34205  selvply1rhmlem2  34206  selvply1rhmlem4  34208  selvply1rhmlem5  34209  selvply1rhm  34210  selvply1rhm0  34211  mvrvalind  34223  mplmulmvr  34224  evlextv  34227  psrmonmul  34235  esplyfval0  34249  esplyfvaln  34259  esplyind  34260  esplyindfv  34261  vietalem  34264  lsatdim  34302  drngdimgt0  34303  dimkerim  34312  evls1fldgencl  34355  algextdeglem1  34402  algextdeglem2  34403  algextdeglem3  34404  algextdeglem4  34405  algextdeglem5  34406  rtelextdg2  34412  constrextdg2lem  34433  constrext2chnlem  34435  constrfiss  34436  qtopt1  34520  locfinref  34526  zarcls0  34553  zarmxt1  34565  zarcmplem  34566  ordtrestNEW  34606  esumsnf  34749  esum2dlem  34777  rossros  34866  oms0  34982  carsggect  35003  eulerpartlems  35045  eulerpartlemgc  35047  eulerpartlemgh  35063  eulerpartlemgs2  35065  circlemeth  35322  hgt750lemb  35338  hgt750leme  35340  bnj1452  35735  subfacp1lem1  36065  subfacp1lem5  36070  erdszelem4  36080  erdszelem8  36084  sconnpi1  36125  cvmscld  36159  cvmlift2lem6  36194  cvmlift2lem9  36197  cvmlift2lem11  36199  cvmlift2lem12  36200  mrsubvrs  36408  ellcsrspsn  36527  neibastop2lem  37275  topjoin  37280  fnejoin2  37284  weiunse  37383  pibt2  38480  lindsadd  38676  poimirlem3  38681  poimirlem9  38687  poimirlem28  38706  poimirlem32  38710  prdsbnd  38867  heiborlem8  38892  rrnequiv  38909  grpokerinj  38967  0idl  39099  prnc  39141  isfldidl  39142  lshpnel2N  40182  lsatfixedN  40206  lfl0f  40266  lkrlsp3  40301  elpaddatriN  41000  elpaddat  41001  elpadd2at  41003  pmodlem1  41043  osumcllem1N  41153  osumcllem2N  41154  osumcllem9N  41161  osumcllem10N  41162  pexmidlem6N  41172  pexmidlem7N  41173  dibss  42366  dochocsn  42578  dochsncom  42579  dochnel  42590  dihprrnlem1N  42621  dihprrnlem2  42622  djhlsmat  42624  dihsmsprn  42627  dvh4dimlem  42640  dvhdimlem  42641  dochsnnz  42647  dochsatshp  42648  dochsnshp  42650  dochexmid  42665  dochsnkr  42669  dochsnkr2cl  42671  dochfl1  42673  lcfl7lem  42696  lcfl6  42697  lcfl8  42699  lcfl9a  42702  lclkrlem2a  42704  lclkrlem2c  42706  lclkrlem2d  42707  lclkrlem2e  42708  lclkrlem2j  42713  lclkrlem2o  42718  lclkrlem2p  42719  lclkrlem2s  42722  lclkrlem2v  42725  lcfrlem14  42753  lcfrlem18  42757  lcfrlem19  42758  lcfrlem20  42759  lcfrlem23  42762  lcfrlem25  42764  lcdlkreqN  42819  mapdval4N  42829  mapdsn  42838  mapdhvmap  42966  hdmaprnlem4tN  43049  hdmapinvlem1  43115  hdmapinvlem2  43116  hdmapinvlem3  43117  hdmapinvlem4  43118  hdmapglem5  43119  hgmapvvlem3  43122  hdmapglem7a  43124  hdmapglem7b  43125  hdmapglem7  43126  hdmapoc  43128  aks6d1c5lem3  43327  deg1gprod  43330  sticksstones9  43344  sticksstones11  43346  rhmqusspan  43375  evlsbagval  43754  0prjspnrel  43803  elrfi  43845  cmpfiiin  43848  mzpcompact2lem  43902  dfac11  44204  pwssplit4  44231  rngunsnply  44311  flcidc  44312  proot1mul  44336  iocinico  44354  cantnfresb  44466  iunrelexp0  44842  frege81d  44887  k0004lem3  45289  mnuunid  45401  binomcxplemnn0  45473  islptre  46770  limciccioolb  46772  limcicciooub  46786  limcresiooub  46791  limcresioolb  46792  ioccncflimc  47034  icccncfext  47036  icocncflimc  47038  cncfiooicc  47043  dvnprodlem2  47096  dirkercncflem2  47253  dirkercncflem3  47254  fourierdlem48  47303  fourierdlem49  47304  fourierdlem79  47334  fourierdlem101  47356  sge0sup  47540  hoidmvlelem2  47745  hoiqssbl  47774  hspmbllem1  47775  hspmbllem2  47776  ovnovollem1  47805  tmachlem-agreeprod  48086  tmachlem-agreesn  48096  fsumsplitsndif  48590  imaelsetpreimafv  48616  perfectALTVlem2  48959  stgrclnbgr0  49202  isubgr3stgrlem3  49205  1hegrlfgr  49369  gsumdifsndf  49417  sepfsepc  50181  discsubc  50317  iinfconstbas  50319