Theorem snssd 4749

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-sn 4589

This theorem is used by:  intidg  5432  sofld  6197  fsnex  7322  fr3nr  7818  resf1extb  7980  resf1ext2b  7981  frrlem13  8354  oeeui  8649  naddunif  8741  naddasslem1  8742  naddasslem2  8743  ecinxp  8851  ralxpmap  8962  xpdom3  9132  domunsn  9184  mapdom3  9206  isinf  9294  ac6sfi  9313  pwfilem  9347  finsschain  9386  ssfii  9448  marypha1lem  9462  unxpwdom2  9619  en2other2  10127  fseqenlem1  10142  axdc3lem4  10570  axdc4lem  10572  ttukeylem7  10632  fpwwe2lem12  10766  canthwe  10775  canthp1lem1  10776  wuncval2  10871  un0addcl  12679  un0mulcl  12680  ssfzunsnext  13743  fseq1p1m1  13772  hashbclem  14638  hashf1lem1  14641  s1f1  14798  fsumsplit1  15955  fsumge1  16008  incexclem  16049  isumltss  16061  fprodsplit1f  16201  rpnnen2lem11  16436  bitsinv1  16656  lcmfunsnlem2  16859  lcmfass  16865  phicl2  16989  vdwlem1  17203  vdwlem8  17210  vdwlem12  17214  vdwlem13  17215  0ram  17242  ramub1lem1  17248  ramub1lem2  17249  ramcl  17251  imasaddfnlem  17750  imasaddflem  17752  imasvscafn  17759  imasvscaf  17761  mrieqvlemd  17853  mreexmrid  17867  mreexexlem4d  17871  acsfiindd  18777  acsmapd  18778  chnccat  18850  gsumress  18921  0subm  19063  gsumvallem2  19080  trivsubgd  19413  trivsubgsnd  19414  trivnsgd  19432  cycsubg2cl  19476  kerf1ghm  19511  pmtrprfv  19718  odf1o1  19837  gex1  19856  sylow2alem1  19882  sylow2alem2  19883  lsm01  19936  lsm02  19937  lsmdisj  19946  lsmdisj2  19947  prmcyg  20159  gsumzadd  20187  gsumconst  20199  gsumdifsnd  20226  gsumpt  20227  gsumxp  20241  dmdprdd  20266  dprdfadd  20287  dprdres  20295  dprdz  20297  dprdsn  20303  dprddisj2  20306  dprd2da  20309  dprd2d2  20311  dmdprdsplit2lem  20312  dpjcntz  20319  dpjdisj  20320  dpjlsm  20321  dpjidcl  20325  ablfacrp  20333  ablfac1eu  20340  pgpfac1lem1  20341  pgpfac1lem3a  20343  pgpfac1lem3  20344  pgpfac1lem5  20346  pgpfaclem2  20349  acsfn1p  21107  lsssn0  21274  lss0ss  21275  lsptpcl  21305  lspsnvsi  21330  lspun0  21337  pwssplit1  21385  lsmpr  21415  lsppr  21419  lspsntri  21423  lspsolvlem  21471  lspsolv  21472  lsppratlem1  21476  lsppratlem3  21478  lsppratlem4  21479  islbs3  21484  lbsextlem4  21490  rnglidl0  21560  0ringidl  21565  rsp1  21571  lidlnz  21581  drngidl  21590  isprmidlc  21679  qsidomlem2  21688  ssdifidlprm  21693  lidldvgen  21709  mulgrhm2  21839  zndvds  21910  psrlidm  22324  psrridm  22325  mplmonmul  22400  selvvvval  22506  mdetdiaglem  22968  mdetrlin  22972  mdetrsca  22973  mdetrsca2  22974  mdetrlin2  22977  mdetunilem5  22986  mdetunilem9  22990  mdetmul  22993  en2top  23358  rest0  23542  ordtrest  23575  iscnp4  23636  cnconst2  23656  cnpdis  23666  ist1-2  23720  cnt1  23723  dishaus  23755  discmp  23771  cmpcld  23775  conncompid  23804  dis2ndc  23834  dislly  23871  dissnref  23902  comppfsc  23906  llycmpkgen2  23924  cmpkgen  23925  1stckgenlem  23927  1stckgen  23928  ptbasfi  23955  txdis  24006  txdis1cn  24009  txcmplem1  24015  xkohaus  24027  xkoptsub  24028  xkoinjcn  24061  snfbas  24240  trnei  24266  isufil2  24282  ufileu  24293  filufint  24294  uffixsn  24299  ufildom1  24300  flimopn  24349  hausflim  24355  flimcf  24356  flimclslem  24358  flimsncls  24360  cnpflf2  24374  cnpflf  24375  fclsneii  24391  fclsfnflim  24401  fcfnei  24409  flfcntr  24417  alexsubALTlem3  24423  alexsubALTlem4  24424  ptcmplem2  24427  cldsubg  24485  snclseqg  24490  qustgphaus  24497  tsmsgsum  24513  tsmsid  24514  tgptsmscld  24525  tsmsxplem1  24527  tsmsxplem2  24528  ust0  24594  ustuqtop1  24615  neipcfilu  24669  prdsdsf  24741  prdsxmetlem  24742  prdsmet  24744  imasdsf1olem  24747  xpsdsval  24755  prdsbl  24865  prdsxmslem2  24903  idnghm  25117  icccmplem2  25198  metnrmlem2  25235  ioombl  25941  volivth  25983  itg11  26067  i1fmulclem  26078  itg2mulclem  26122  itgsplitioo  26213  limcvallem  26246  limcdif  26251  ellimc2  26252  limcflf  26256  limcmpt2  26259  limcres  26261  cnplimc  26262  limccnp  26266  limccnp2  26267  limcco  26268  dvreslem  26284  dvaddbr  26313  dvmulbr  26314  dvcmulf  26320  dvef  26355  dvivth  26385  lhop2  26390  lhop  26391  ply1remlem  26538  fta1blem  26544  ig1peu  26548  ig1pdvds  26553  plyco0  26565  elply2  26569  plyf  26571  elplyr  26574  elplyd  26575  ply1term  26577  ply0  26581  plyeq0lem  26584  plyeq0  26585  plypf1  26586  plyaddlem  26589  plymullem  26590  dgrlem  26603  coef2  26605  coeidlem  26611  plyco  26615  coemulhi  26628  plycj  26651  plyn0mulidp  26657  vieta1  26690  rngunsnply  26693  taylf  26745  radcnv0  26800  abelth  26825  rlimcnp  27350  xrlimcnp  27353  amgm  27375  wilthlem2  27453  basellem7  27471  basellem9  27473  ppiprm  27535  chtprm  27537  musumsum  27576  muinv  27577  logexprlim  27609  perfectlem2  27614  dchrhash  27655  rpvmasum2  27896  sltssnb  28212  conway  28222  lesrec  28242  eqcuts3  28247  cofcutr  28367  cutlt  28375  cutmax  28377  cutmin  28378  cutminmax  28379  addsuniflem  28444  negsunif  28498  sltmuls1  28590  sltmuls2  28591  precsexlem11  28660  oncutlt  28707  n0fincut  28798  bdaypw2n0bndlem  28906  axlowdimlem7  29583  axlowdimlem10  29586  upgrex  29727  upgr1elem  29747  uvtxnm1nbgr  30042  umgr2v2e  30163  pthhashvtx  30372  cyclnumvtx  30445  0oo  31448  sh0le  32099  disjiunel  33288  preimane  33361  fnpreimac  33362  fsuppinisegfi  33377  fprodeq02  33511  indsn  33526  gsumzresunsn  33722  gsumhashmul  33727  pmtrcnelor  33751  edompidlem  33960  primefldgen1  33987  dvdsrspss  34046  elgrplsmsn  34049  lsmsnorb  34050  grplsm0l  34058  grplsmid  34059  unitpidl1  34078  elrspunsn  34083  mxidlprm  34099  mxidlirredi  34100  mxidlirred  34101  drngmxidl  34105  drngmxidlr  34106  qsdrngilem  34122  dflringlem  34130  rsprprmprmidl  34158  rprmirredb  34168  1arithufdlem4  34183  evls1rgspncl  34248  rngunsnply1  34249  selvply1rhmlem1  34263  selvply1rhmlem2  34264  selvply1rhmlem4  34266  selvply1rhmlem5  34267  selvply1rhm  34268  selvply1rhm0  34269  mvrvalind  34281  mplmulmvr  34282  evlextv  34285  psrmonmul  34293  esplyfval0  34307  esplyfvaln  34317  esplyind  34318  esplyindfv  34319  vietalem  34322  lsatdim  34360  drngdimgt0  34361  dimkerim  34370  evls1fldgencl  34413  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  rtelextdg2  34470  constrextdg2lem  34491  constrext2chnlem  34493  constrfiss  34494  qtopt1  34578  locfinref  34584  zarcls0  34611  zarmxt1  34623  zarcmplem  34624  ordtrestNEW  34664  esumsnf  34807  esum2dlem  34835  rossros  34924  oms0  35040  carsggect  35061  eulerpartlems  35103  eulerpartlemgc  35105  eulerpartlemgh  35121  eulerpartlemgs2  35123  circlemeth  35380  hgt750lemb  35396  hgt750leme  35398  bnj1452  35793  subfacp1lem1  36152  subfacp1lem5  36157  erdszelem4  36167  erdszelem8  36171  sconnpi1  36212  cvmscld  36246  cvmlift2lem6  36281  cvmlift2lem9  36284  cvmlift2lem11  36286  cvmlift2lem12  36287  mrsubvrs  36495  ellcsrspsn  36614  neibastop2lem  37363  topjoin  37368  fnejoin2  37372  weiunse  37471  pibt2  38608  lindsadd  38804  poimirlem3  38809  poimirlem9  38815  poimirlem28  38834  poimirlem32  38838  prdsbnd  38993  heiborlem8  39018  rrnequiv  39035  grpokerinj  39093  0idl  39225  prnc  39267  isfldidl  39268  lshpnel2N  40308  lsatfixedN  40332  lfl0f  40392  lkrlsp3  40427  elpaddatriN  41126  elpaddat  41127  elpadd2at  41129  pmodlem1  41169  osumcllem1N  41279  osumcllem2N  41280  osumcllem9N  41287  osumcllem10N  41288  pexmidlem6N  41298  pexmidlem7N  41299  dibss  42492  dochocsn  42704  dochsncom  42705  dochnel  42716  dihprrnlem1N  42747  dihprrnlem2  42748  djhlsmat  42750  dihsmsprn  42753  dvh4dimlem  42766  dvhdimlem  42767  dochsnnz  42773  dochsatshp  42774  dochsnshp  42776  dochexmid  42791  dochsnkr  42795  dochsnkr2cl  42797  dochfl1  42799  lcfl7lem  42822  lcfl6  42823  lcfl8  42825  lcfl9a  42828  lclkrlem2a  42830  lclkrlem2c  42832  lclkrlem2d  42833  lclkrlem2e  42834  lclkrlem2j  42839  lclkrlem2o  42844  lclkrlem2p  42845  lclkrlem2s  42848  lclkrlem2v  42851  lcfrlem14  42879  lcfrlem18  42883  lcfrlem19  42884  lcfrlem20  42885  lcfrlem23  42888  lcfrlem25  42890  lcdlkreqN  42945  mapdval4N  42955  mapdsn  42964  mapdhvmap  43092  hdmaprnlem4tN  43175  hdmapinvlem1  43241  hdmapinvlem2  43242  hdmapinvlem3  43243  hdmapinvlem4  43244  hdmapglem5  43245  hgmapvvlem3  43248  hdmapglem7a  43250  hdmapglem7b  43251  hdmapglem7  43252  hdmapoc  43254  aks6d1c5lem3  43453  deg1gprod  43456  sticksstones9  43470  sticksstones11  43472  rhmqusspan  43501  evlsbagval  43880  0prjspnrel  43929  elrfi  43971  cmpfiiin  43974  mzpcompact2lem  44028  dfac11  44330  pwssplit4  44357  flcidc  44433  proot1mul  44457  iocinico  44475  cantnfresb  44587  iunrelexp0  44963  frege81d  45008  k0004lem3  45410  mnuunid  45522  binomcxplemnn0  45594  islptre  46904  limciccioolb  46906  limcicciooub  46920  limcresiooub  46925  limcresioolb  46926  ioccncflimc  47168  icccncfext  47170  icocncflimc  47172  cncfiooicc  47177  dvnprodlem2  47230  dirkercncflem2  47387  dirkercncflem3  47388  fourierdlem48  47437  fourierdlem49  47438  fourierdlem79  47468  fourierdlem101  47490  sge0sup  47674  hoidmvlelem2  47879  hoiqssbl  47908  hspmbllem1  47909  hspmbllem2  47910  ovnovollem1  47939  tmachlem-agreeprod  48220  tmachlem-agreesn  48230  fsumsplitsndif  48724  imaelsetpreimafv  48750  perfectALTVlem2  49093  stgrclnbgr0  49336  isubgr3stgrlem3  49339  1hegrlfgr  49503  gsumdifsndf  49551  sepfsepc  50373  discsubc  50509  iinfconstbas  50511