Theorem snssd 4754

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-sn 4592

This theorem is used by:  intidg  5440  sofld  6187  fsnex  7290  fr3nr  7777  resf1extb  7937  resf1ext2b  7938  frrlem13  8301  oeeui  8594  naddunif  8686  naddasslem1  8687  naddasslem2  8688  ecinxp  8796  ralxpmap  8900  xpdom3  9070  domunsn  9122  mapdom3  9144  isinf  9232  ac6sfi  9251  pwfilem  9284  finsschain  9323  ssfii  9386  marypha1lem  9400  unxpwdom2  9557  en2other2  10009  fseqenlem1  10024  axdc3lem4  10452  axdc4lem  10454  ttukeylem7  10514  fpwwe2lem12  10644  canthwe  10653  canthp1lem1  10654  wuncval2  10749  un0addcl  12554  un0mulcl  12555  ssfzunsnext  13616  fseq1p1m1  13645  hashbclem  14509  hashf1lem1  14512  s1f1  14668  fsumsplit1  15821  fsumge1  15874  incexclem  15915  isumltss  15927  fprodsplit1f  16069  rpnnen2lem11  16304  bitsinv1  16524  lcmfunsnlem2  16722  lcmfass  16728  phicl2  16851  vdwlem1  17065  vdwlem8  17072  vdwlem12  17076  vdwlem13  17077  0ram  17104  ramub1lem1  17110  ramub1lem2  17111  ramcl  17113  imasaddfnlem  17606  imasaddflem  17608  imasvscafn  17615  imasvscaf  17617  mrieqvlemd  17709  mreexmrid  17723  mreexexlem4d  17727  acsfiindd  18633  acsmapd  18634  chnccat  18706  gsumress  18774  0subm  18915  gsumvallem2  18932  trivsubgd  19265  trivsubgsnd  19266  trivnsgd  19284  cycsubg2cl  19328  kerf1ghm  19363  pmtrprfv  19569  odf1o1  19688  gex1  19707  sylow2alem1  19733  sylow2alem2  19734  lsm01  19787  lsm02  19788  lsmdisj  19797  lsmdisj2  19798  prmcyg  20010  gsumzadd  20038  gsumconst  20050  gsumdifsnd  20077  gsumpt  20078  gsumxp  20092  dmdprdd  20117  dprdfadd  20138  dprdres  20146  dprdz  20148  dprdsn  20154  dprddisj2  20157  dprd2da  20160  dprd2d2  20162  dmdprdsplit2lem  20163  dpjcntz  20170  dpjdisj  20171  dpjlsm  20172  dpjidcl  20176  ablfacrp  20184  ablfac1eu  20191  pgpfac1lem1  20192  pgpfac1lem3a  20194  pgpfac1lem3  20195  pgpfac1lem5  20197  pgpfaclem2  20200  acsfn1p  20954  lsssn0  21121  lss0ss  21122  lsptpcl  21152  lspsnvsi  21177  lspun0  21184  pwssplit1  21232  lsmpr  21262  lsppr  21266  lspsntri  21270  lspsolvlem  21318  lspsolv  21319  lsppratlem1  21323  lsppratlem3  21325  lsppratlem4  21326  islbs3  21331  lbsextlem4  21337  rnglidl0  21407  0ringidl  21412  rsp1  21418  lidlnz  21428  drngidl  21437  isprmidlc  21524  qsidomlem2  21533  ssdifidlprm  21538  lidldvgen  21554  mulgrhm2  21680  zndvds  21751  psrlidm  22163  psrridm  22164  mplmonmul  22239  selvvvval  22345  mdetdiaglem  22807  mdetrlin  22811  mdetrsca  22812  mdetrsca2  22813  mdetrlin2  22816  mdetunilem5  22825  mdetunilem9  22829  mdetmul  22832  en2top  23194  rest0  23378  ordtrest  23411  iscnp4  23472  cnconst2  23492  cnpdis  23502  ist1-2  23556  cnt1  23559  dishaus  23591  discmp  23607  cmpcld  23611  conncompid  23640  dis2ndc  23670  dislly  23707  dissnref  23738  comppfsc  23742  llycmpkgen2  23760  cmpkgen  23761  1stckgenlem  23763  1stckgen  23764  ptbasfi  23791  txdis  23842  txdis1cn  23845  txcmplem1  23851  xkohaus  23863  xkoptsub  23864  xkoinjcn  23897  snfbas  24076  trnei  24102  isufil2  24118  ufileu  24129  filufint  24130  uffixsn  24135  ufildom1  24136  flimopn  24185  hausflim  24191  flimcf  24192  flimclslem  24194  flimsncls  24196  cnpflf2  24210  cnpflf  24211  fclsneii  24227  fclsfnflim  24237  fcfnei  24245  flfcntr  24253  alexsubALTlem3  24259  alexsubALTlem4  24260  ptcmplem2  24263  cldsubg  24321  snclseqg  24326  qustgphaus  24333  tsmsgsum  24349  tsmsid  24350  tgptsmscld  24361  tsmsxplem1  24363  tsmsxplem2  24364  ust0  24430  ustuqtop1  24451  neipcfilu  24505  prdsdsf  24577  prdsxmetlem  24578  prdsmet  24580  imasdsf1olem  24583  xpsdsval  24591  prdsbl  24701  prdsxmslem2  24739  idnghm  24953  icccmplem2  25034  metnrmlem2  25071  ioombl  25777  volivth  25819  itg11  25903  i1fmulclem  25914  itg2mulclem  25958  itgsplitioo  26050  limcvallem  26083  limcdif  26088  ellimc2  26089  limcflf  26093  limcmpt2  26096  limcres  26098  cnplimc  26099  limccnp  26103  limccnp2  26104  limcco  26105  dvreslem  26121  dvaddbr  26150  dvmulbr  26151  dvcmulf  26157  dvef  26192  dvivth  26222  lhop2  26227  lhop  26228  ply1remlem  26375  fta1blem  26381  ig1peu  26385  ig1pdvds  26390  plyco0  26402  elply2  26406  plyf  26408  elplyr  26411  elplyd  26412  ply1term  26414  ply0  26418  plyeq0lem  26420  plyeq0  26421  plypf1  26422  plyaddlem  26425  plymullem  26426  dgrlem  26439  coef2  26441  coeidlem  26447  plyco  26451  coemulhi  26464  plycj  26487  plycjOLD  26489  plyn0mulidp  26495  vieta1  26526  taylf  26577  radcnv0  26632  abelth  26657  rlimcnp  27183  xrlimcnp  27186  amgm  27208  wilthlem2  27286  basellem7  27304  basellem9  27306  ppiprm  27368  chtprm  27370  musumsum  27409  muinv  27410  logexprlim  27442  perfectlem2  27447  dchrhash  27488  rpvmasum2  27729  sltssnb  28015  conway  28025  lesrec  28045  eqcuts3  28050  cofcutr  28170  cutlt  28178  cutmax  28180  cutmin  28181  cutminmax  28182  addsuniflem  28247  negsunif  28301  sltmuls1  28393  sltmuls2  28394  precsexlem11  28463  oncutlt  28510  n0fincut  28601  bdaypw2n0bndlem  28709  axlowdimlem7  29355  axlowdimlem10  29358  upgrex  29499  upgr1elem  29519  uvtxnm1nbgr  29814  umgr2v2e  29935  pthhashvtx  30144  cyclnumvtx  30217  0oo  31214  sh0le  31865  disjiunel  33014  preimane  33087  fnpreimac  33088  fsuppinisegfi  33105  fprodeq02  33240  indsn  33255  gsumzresunsn  33448  gsumhashmul  33453  pmtrcnelor  33477  primefldgen1  33708  dvdsrspss  33766  elgrplsmsn  33769  lsmsnorb  33770  grplsm0l  33778  grplsmid  33779  unitpidl1  33798  elrspunsn  33803  mxidlprm  33819  mxidlirredi  33820  mxidlirred  33821  drngmxidl  33825  drngmxidlr  33826  qsdrngilem  33842  dflringlem  33850  rsprprmprmidl  33878  rprmirredb  33888  1arithufdlem4  33903  selvply1rhmlem1  33976  selvply1rhmlem2  33977  selvply1rhmlem4  33979  selvply1rhmlem5  33980  selvply1rhm  33981  selvply1rhm0  33982  mvrvalind  33994  mplmulmvr  33995  evlextv  33998  psrmonmul  34006  esplyfval0  34020  esplyfvaln  34030  esplyind  34031  esplyindfv  34032  vietalem  34035  lsatdim  34073  drngdimgt0  34074  dimkerim  34083  evls1fldgencl  34126  algextdeglem1  34173  algextdeglem2  34174  algextdeglem3  34175  algextdeglem4  34176  algextdeglem5  34177  rtelextdg2  34183  constrextdg2lem  34204  constrext2chnlem  34206  constrfiss  34207  qtopt1  34291  locfinref  34297  zarcls0  34324  zarmxt1  34336  zarcmplem  34337  ordtrestNEW  34377  esumsnf  34520  esum2dlem  34548  rossros  34637  oms0  34754  carsggect  34775  eulerpartlems  34817  eulerpartlemgc  34819  eulerpartlemgh  34835  eulerpartlemgs2  34837  circlemeth  35094  hgt750lemb  35110  hgt750leme  35112  bnj1452  35507  subfacp1lem1  35710  subfacp1lem5  35715  erdszelem4  35725  erdszelem8  35729  sconnpi1  35770  cvmscld  35804  cvmlift2lem6  35839  cvmlift2lem9  35842  cvmlift2lem11  35844  cvmlift2lem12  35845  mrsubvrs  36053  ellcsrspsn  36172  neibastop2lem  36930  topjoin  36935  fnejoin2  36939  weiunse  37038  pibt2  38122  lindsadd  38323  poimirlem3  38333  poimirlem9  38339  poimirlem28  38358  poimirlem32  38362  prdsbnd  38504  heiborlem8  38529  rrnequiv  38546  grpokerinj  38604  0idl  38736  prnc  38778  isfldidl  38779  lshpnel2N  39819  lsatfixedN  39843  lfl0f  39903  lkrlsp3  39938  elpaddatriN  40637  elpaddat  40638  elpadd2at  40640  pmodlem1  40680  osumcllem1N  40790  osumcllem2N  40791  osumcllem9N  40798  osumcllem10N  40799  pexmidlem6N  40809  pexmidlem7N  40810  dibss  42003  dochocsn  42215  dochsncom  42216  dochnel  42227  dihprrnlem1N  42258  dihprrnlem2  42259  djhlsmat  42261  dihsmsprn  42264  dvh4dimlem  42277  dvhdimlem  42278  dochsnnz  42284  dochsatshp  42285  dochsnshp  42287  dochexmid  42302  dochsnkr  42306  dochsnkr2cl  42308  dochfl1  42310  lcfl7lem  42333  lcfl6  42334  lcfl8  42336  lcfl9a  42339  lclkrlem2a  42341  lclkrlem2c  42343  lclkrlem2d  42344  lclkrlem2e  42345  lclkrlem2j  42350  lclkrlem2o  42355  lclkrlem2p  42356  lclkrlem2s  42359  lclkrlem2v  42362  lcfrlem14  42390  lcfrlem18  42394  lcfrlem19  42395  lcfrlem20  42396  lcfrlem23  42399  lcfrlem25  42401  lcdlkreqN  42456  mapdval4N  42466  mapdsn  42475  mapdhvmap  42603  hdmaprnlem4tN  42686  hdmapinvlem1  42752  hdmapinvlem2  42753  hdmapinvlem3  42754  hdmapinvlem4  42755  hdmapglem5  42756  hgmapvvlem3  42759  hdmapglem7a  42761  hdmapglem7b  42762  hdmapglem7  42763  hdmapoc  42765  aks6d1c5lem3  42964  deg1gprod  42967  sticksstones9  42981  sticksstones11  42983  rhmqusspan  43012  evlsbagval  43378  0prjspnrel  43419  elrfi  43485  cmpfiiin  43488  mzpcompact2lem  43542  dfac11  43849  pwssplit4  43876  rngunsnply  43956  flcidc  43957  proot1mul  43981  iocinico  43999  cantnfresb  44111  iunrelexp0  44488  frege81d  44533  k0004lem3  44935  mnuunid  45047  binomcxplemnn0  45119  islptre  46395  limciccioolb  46397  limcicciooub  46411  limcresiooub  46416  limcresioolb  46417  ioccncflimc  46659  icccncfext  46661  icocncflimc  46663  cncfiooicc  46668  dvnprodlem2  46721  dirkercncflem2  46878  dirkercncflem3  46879  fourierdlem48  46928  fourierdlem49  46929  fourierdlem79  46959  fourierdlem101  46981  sge0sup  47165  hoidmvlelem2  47370  hoiqssbl  47399  hspmbllem1  47400  hspmbllem2  47401  ovnovollem1  47430  fsumsplitsndif  48178  imaelsetpreimafv  48204  perfectALTVlem2  48547  stgrclnbgr0  48790  isubgr3stgrlem3  48793  1hegrlfgr  48957  gsumdifsndf  49005  sepfsepc  49765  discsubc  49901  iinfconstbas  49903