Theorem snssd 4742

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-sn 4568

This theorem is referenced by:  sofld  6044  fsnex  7039  fr3nr  7494  wfrlem15  7969  oeeui  8228  ecinxp  8372  ralxpmap  8460  xpdom3  8615  domunsn  8667  mapdom3  8689  isinf  8731  ac6sfi  8762  pwfilem  8818  finsschain  8831  ssfii  8883  marypha1lem  8897  unxpwdom2  9052  en2other2  9435  fseqenlem1  9450  axdc3lem4  9875  axdc4lem  9877  ttukeylem7  9937  fpwwe2lem13  10064  canthwe  10073  canthp1lem1  10074  wuncval2  10169  un0addcl  11931  un0mulcl  11932  ssfzunsnext  12953  fseq1p1m1  12982  hashbclem  13811  hashf1lem1  13814  fsumge1  15152  incexclem  15191  isumltss  15203  fprodsplit1f  15344  rpnnen2lem11  15577  bitsinv1  15791  lcmfunsnlem2  15984  lcmfass  15990  phicl2  16105  vdwlem1  16317  vdwlem8  16324  vdwlem12  16328  vdwlem13  16329  0ram  16356  ramub1lem1  16362  ramub1lem2  16363  ramcl  16365  imasaddfnlem  16801  imasaddflem  16803  imasvscafn  16810  imasvscaf  16812  mrieqvlemd  16900  mreexmrid  16914  mreexexlem4d  16918  acsfiindd  17787  acsmapd  17788  gsumress  17892  0subm  17982  gsumvallem2  17998  0subg  18304  trivsubgd  18305  trivsubgsnd  18306  trivnsgd  18324  cycsubg2cl  18354  pmtrprfv  18581  odf1o1  18697  gex1  18716  sylow2alem1  18742  sylow2alem2  18743  lsm01  18797  lsm02  18798  lsmdisj  18807  lsmdisj2  18808  prmcyg  19014  gsumzadd  19042  gsumconst  19054  gsumdifsnd  19081  gsumpt  19082  gsumxp  19096  dmdprdd  19121  dprdfadd  19142  dprdres  19150  dprdz  19152  dprdsn  19158  dprddisj2  19161  dprd2da  19164  dprd2d2  19166  dmdprdsplit2lem  19167  dpjcntz  19174  dpjdisj  19175  dpjlsm  19176  dpjidcl  19180  ablfacrp  19188  ablfac1eu  19195  pgpfac1lem1  19196  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem5  19201  pgpfaclem2  19204  kerf1ghm  19497  kerf1hrmOLD  19498  acsfn1p  19578  lsssn0  19719  lss0ss  19720  lsptpcl  19751  lspsnvsi  19776  lspun0  19783  pwssplit1  19831  lsmpr  19861  lsppr  19865  lspsntri  19869  lspsolvlem  19914  lspsolv  19915  lsppratlem1  19919  lsppratlem3  19921  lsppratlem4  19922  islbs3  19927  lbsextlem4  19933  rsp1  19997  lidlnz  20001  lidldvgen  20028  psrlidm  20183  psrridm  20184  mplmonmul  20245  mulgrhm2  20646  zndvds  20696  mdetdiaglem  21207  mdetrlin  21211  mdetrsca  21212  mdetrsca2  21213  mdetrlin2  21216  mdetunilem5  21225  mdetunilem9  21229  mdetmul  21232  en2top  21593  rest0  21777  ordtrest  21810  iscnp4  21871  cnconst2  21891  cnpdis  21901  ist1-2  21955  cnt1  21958  dishaus  21990  discmp  22006  cmpcld  22010  conncompid  22039  dis2ndc  22068  dislly  22105  dissnref  22136  comppfsc  22140  llycmpkgen2  22158  cmpkgen  22159  1stckgenlem  22161  1stckgen  22162  ptbasfi  22189  txdis  22240  txdis1cn  22243  txcmplem1  22249  xkohaus  22261  xkoptsub  22262  xkoinjcn  22295  snfbas  22474  trnei  22500  isufil2  22516  ufileu  22527  filufint  22528  uffixsn  22533  ufildom1  22534  flimopn  22583  hausflim  22589  flimcf  22590  flimclslem  22592  flimsncls  22594  cnpflf2  22608  cnpflf  22609  fclsneii  22625  fclsfnflim  22635  fcfnei  22643  flfcntr  22651  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  cldsubg  22719  snclseqg  22724  qustgphaus  22731  tsmsgsum  22747  tsmsid  22748  tgptsmscld  22759  tsmsxplem1  22761  tsmsxplem2  22762  ust0  22828  ustuqtop1  22850  neipcfilu  22905  prdsdsf  22977  prdsxmetlem  22978  prdsmet  22980  imasdsf1olem  22983  xpsdsval  22991  prdsbl  23101  prdsxmslem2  23139  idnghm  23352  icccmplem2  23431  metnrmlem2  23468  ioombl  24166  volivth  24208  itg11  24292  i1fmulclem  24303  itg2mulclem  24347  itgsplitioo  24438  limcvallem  24469  limcdif  24474  ellimc2  24475  limcflf  24479  limcmpt2  24482  limcres  24484  cnplimc  24485  limccnp  24489  limccnp2  24490  limcco  24491  dvreslem  24507  dvaddbr  24535  dvmulbr  24536  dvcmulf  24542  dvef  24577  dvivth  24607  lhop2  24612  lhop  24613  ply1remlem  24756  fta1blem  24762  ig1peu  24765  ig1pdvds  24770  plyco0  24782  elply2  24786  plyf  24788  elplyr  24791  elplyd  24792  ply1term  24794  ply0  24798  plyeq0lem  24800  plyeq0  24801  plypf1  24802  plyaddlem  24805  plymullem  24806  dgrlem  24819  coef2  24821  coeidlem  24827  plyco  24831  coemulhi  24844  plycj  24867  vieta1  24901  taylf  24949  radcnv0  25004  abelth  25029  rlimcnp  25543  xrlimcnp  25546  amgm  25568  wilthlem2  25646  basellem7  25664  basellem9  25666  ppiprm  25728  chtprm  25730  musumsum  25769  muinv  25770  logexprlim  25801  perfectlem2  25806  dchrhash  25847  rpvmasum2  26088  axlowdimlem7  26734  axlowdimlem10  26737  upgrex  26877  upgr1elem  26897  uvtxnm1nbgr  27186  umgr2v2e  27307  0oo  28566  sh0le  29217  disjiunel  30346  preimane  30415  fnpreimac  30416  fprodeq02  30539  s1f1  30619  gsumzresunsn  30691  pmtrcnelor  30735  elgrplsmsn  30944  lsmsnorb  30945  isprmidlc  30963  qsidomlem2  30966  mxidlprm  30977  lsatdim  31015  drngdimgt0  31016  dimkerim  31023  qtopt1  31099  locfinref  31105  ordtrestNEW  31164  esumsnf  31323  esum2dlem  31351  rossros  31439  oms0  31555  carsggect  31576  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemgh  31636  eulerpartlemgs2  31638  plymulx0  31817  circlemeth  31911  hgt750lemb  31927  hgt750leme  31929  bnj1452  32324  pthhashvtx  32374  subfacp1lem1  32426  subfacp1lem5  32431  erdszelem4  32441  erdszelem8  32445  sconnpi1  32486  cvmscld  32520  cvmlift2lem6  32555  cvmlift2lem9  32558  cvmlift2lem11  32560  cvmlift2lem12  32561  mrsubvrs  32769  frrlem13  33135  slerec  33277  neibastop2lem  33708  topjoin  33713  fnejoin2  33717  pibt2  34701  lindsadd  34900  poimirlem3  34910  poimirlem9  34916  poimirlem28  34935  poimirlem32  34939  prdsbnd  35086  heiborlem8  35111  rrnequiv  35128  grpokerinj  35186  0idl  35318  prnc  35360  isfldidl  35361  lshpnel2N  36136  lsatfixedN  36160  lfl0f  36220  lkrlsp3  36255  elpaddatriN  36954  elpaddat  36955  elpadd2at  36957  pmodlem1  36997  osumcllem1N  37107  osumcllem2N  37108  osumcllem9N  37115  osumcllem10N  37116  pexmidlem6N  37126  pexmidlem7N  37127  dibss  38320  dochocsn  38532  dochsncom  38533  dochnel  38544  dihprrnlem1N  38575  dihprrnlem2  38576  djhlsmat  38578  dihsmsprn  38581  dvh4dimlem  38594  dvhdimlem  38595  dochsnnz  38601  dochsatshp  38602  dochsnshp  38604  dochexmid  38619  dochsnkr  38623  dochsnkr2cl  38625  dochfl1  38627  lcfl7lem  38650  lcfl6  38651  lcfl8  38653  lcfl9a  38656  lclkrlem2a  38658  lclkrlem2c  38660  lclkrlem2d  38661  lclkrlem2e  38662  lclkrlem2j  38667  lclkrlem2o  38672  lclkrlem2p  38673  lclkrlem2s  38676  lclkrlem2v  38679  lcfrlem14  38707  lcfrlem18  38711  lcfrlem19  38712  lcfrlem20  38713  lcfrlem23  38716  lcfrlem25  38718  lcdlkreqN  38773  mapdval4N  38783  mapdsn  38792  mapdhvmap  38920  hdmaprnlem4tN  39003  hdmapinvlem1  39069  hdmapinvlem2  39070  hdmapinvlem3  39071  hdmapinvlem4  39072  hdmapglem5  39073  hgmapvvlem3  39076  hdmapglem7a  39078  hdmapglem7b  39079  hdmapglem7  39080  hdmapoc  39082  0prjspnrel  39289  elrfi  39311  cmpfiiin  39314  mzpcompact2lem  39368  dfac11  39682  pwssplit4  39709  rngunsnply  39793  flcidc  39794  proot1mul  39819  iocinico  39838  iunrelexp0  40067  frege81d  40112  k0004lem3  40519  mnuunid  40633  binomcxplemnn0  40701  fsumsplit1  41873  islptre  41920  limciccioolb  41922  limcicciooub  41938  limcresiooub  41943  limcresioolb  41944  ioccncflimc  42188  icccncfext  42190  icocncflimc  42192  cncfiooicc  42197  dvnprodlem2  42252  dirkercncflem2  42409  dirkercncflem3  42410  fourierdlem48  42459  fourierdlem49  42460  fourierdlem79  42490  fourierdlem101  42512  sge0sup  42693  hoidmvlelem2  42898  hoiqssbl  42927  hspmbllem1  42928  hspmbllem2  42929  ovnovollem1  42958  fsumsplitsndif  43553  imaelsetpreimafv  43575  perfectALTVlem2  43907  1hegrlfgr  44027  gsumdifsndf  44108