MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snssd Structured version   Visualization version   GIF version

Theorem snssd 4372
Description: The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
snssd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
snssd (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2 (𝜑𝐴𝐵)
2 snssi 4371 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wss 3607  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-sn 4211
This theorem is referenced by:  sofld  5616  fsnex  6578  fr3nr  7021  wfrlem15  7474  oeeui  7727  ecinxp  7865  ralxpmap  7949  xpdom3  8099  domunsn  8151  mapdom3  8173  isinf  8214  ac6sfi  8245  pwfilem  8301  finsschain  8314  ssfii  8366  marypha1lem  8380  unxpwdom2  8534  en2other2  8870  fseqenlem1  8885  axdc3lem4  9313  axdc4lem  9315  ttukeylem7  9375  fpwwe2lem13  9502  canthwe  9511  canthp1lem1  9512  wuncval2  9607  un0addcl  11364  un0mulcl  11365  ssfzunsnext  12424  fseq1p1m1  12452  hashbclem  13274  hashf1lem1  13277  fsumge1  14573  incexclem  14612  isumltss  14624  rpnnen2lem11  14997  bitsinv1  15211  lcmfunsnlem2  15400  lcmfass  15406  phicl2  15520  vdwlem1  15732  vdwlem8  15739  vdwlem12  15743  vdwlem13  15744  0ram  15771  ramub1lem1  15777  ramub1lem2  15778  ramcl  15780  imasaddfnlem  16235  imasaddflem  16237  imasvscafn  16244  imasvscaf  16246  mrieqvlemd  16336  mreexmrid  16350  mreexexlem4d  16354  acsfiindd  17224  acsmapd  17225  gsumress  17323  gsumvallem2  17419  0subg  17666  cycsubg2cl  17679  pmtrprfv  17919  odf1o1  18033  gex1  18052  sylow2alem1  18078  sylow2alem2  18079  lsm01  18130  lsm02  18131  lsmdisj  18140  lsmdisj2  18141  prmcyg  18341  gsumzadd  18368  gsumconst  18380  gsumdifsnd  18406  gsumpt  18407  gsumxp  18421  dmdprdd  18444  dprdfadd  18465  dprdres  18473  dprdz  18475  dprdsn  18481  dprddisj2  18484  dprd2da  18487  dprd2d2  18489  dmdprdsplit2lem  18490  dpjcntz  18497  dpjdisj  18498  dpjlsm  18499  dpjidcl  18503  ablfacrp  18511  ablfac1eu  18518  pgpfac1lem1  18519  pgpfac1lem3a  18521  pgpfac1lem3  18522  pgpfac1lem5  18524  pgpfaclem2  18527  kerf1hrm  18791  lsssn0  18996  lss0ss  18997  lsptpcl  19027  lspsnvsi  19052  lspun0  19059  pwssplit1  19107  lsmpr  19137  lsppr  19141  lspsntri  19145  lspsolvlem  19190  lspsolv  19191  lsppratlem1  19195  lsppratlem3  19197  lsppratlem4  19198  islbs3  19203  lbsextlem4  19209  rsp1  19272  lidlnz  19276  lidldvgen  19303  psrlidm  19451  psrridm  19452  mplmonmul  19512  mulgrhm2  19895  zndvds  19946  mdetdiaglem  20452  mdetrlin  20456  mdetrsca  20457  mdetrsca2  20458  mdetrlin2  20461  mdetunilem5  20470  mdetunilem9  20474  mdetmul  20477  en2top  20837  rest0  21021  ordtrest  21054  iscnp4  21115  cnconst2  21135  cnpdis  21145  ist1-2  21199  cnt1  21202  dishaus  21234  discmp  21249  cmpcld  21253  conncompid  21282  dis2ndc  21311  dislly  21348  dissnref  21379  comppfsc  21383  llycmpkgen2  21401  cmpkgen  21402  1stckgenlem  21404  1stckgen  21405  ptbasfi  21432  txdis  21483  txdis1cn  21486  txcmplem1  21492  xkohaus  21504  xkoptsub  21505  xkoinjcn  21538  snfbas  21717  trnei  21743  isufil2  21759  ufileu  21770  filufint  21771  uffixsn  21776  ufildom1  21777  flimopn  21826  hausflim  21832  flimcf  21833  flimclslem  21835  flimsncls  21837  cnpflf2  21851  cnpflf  21852  fclsneii  21868  fclsfnflim  21878  fcfnei  21886  flfcntr  21894  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem2  21904  cldsubg  21961  snclseqg  21966  qustgphaus  21973  tsmsgsum  21989  tsmsid  21990  tgptsmscld  22001  tsmsxplem1  22003  tsmsxplem2  22004  ust0  22070  ustuqtop1  22092  neipcfilu  22147  prdsdsf  22219  prdsxmetlem  22220  prdsmet  22222  imasdsf1olem  22225  xpsdsval  22233  prdsbl  22343  prdsxmslem2  22381  idnghm  22594  icccmplem2  22673  metnrmlem2  22710  ioombl  23379  volivth  23421  itg11  23503  i1fmulclem  23514  itg2mulclem  23558  itgsplitioo  23649  limcvallem  23680  limcdif  23685  ellimc2  23686  limcflf  23690  limcmpt2  23693  limcres  23695  cnplimc  23696  limccnp  23700  limccnp2  23701  limcco  23702  dvreslem  23718  dvaddbr  23746  dvmulbr  23747  dvcmulf  23753  dvef  23788  dvivth  23818  lhop2  23823  lhop  23824  ply1remlem  23967  fta1blem  23973  ig1peu  23976  ig1pdvds  23981  plyco0  23993  elply2  23997  plyf  23999  elplyr  24002  elplyd  24003  ply1term  24005  ply0  24009  plyeq0lem  24011  plyeq0  24012  plypf1  24013  plyaddlem  24016  plymullem  24017  dgrlem  24030  coef2  24032  coeidlem  24038  plyco  24042  coemulhi  24055  plycj  24078  vieta1  24112  taylf  24160  radcnv0  24215  abelth  24240  rlimcnp  24737  xrlimcnp  24740  amgm  24762  wilthlem2  24840  basellem7  24858  basellem9  24860  ppiprm  24922  chtprm  24924  musumsum  24963  muinv  24964  logexprlim  24995  perfectlem2  25000  dchrhash  25041  rpvmasum2  25246  axlowdimlem7  25873  axlowdimlem10  25876  upgrex  26032  upgr1elem  26052  uvtxnm1nbgr  26355  umgr2v2e  26477  0oo  27772  sh0le  28427  disjiunel  29535  fprodeq02  29697  qtopt1  30030  locfinref  30036  ordtrestNEW  30095  esumsnf  30254  esum2dlem  30282  rossros  30371  oms0  30487  carsggect  30508  eulerpartlems  30550  eulerpartlemgc  30552  eulerpartlemgh  30568  eulerpartlemgs2  30570  plymulx0  30752  circlemeth  30846  hgt750lemb  30862  hgt750leme  30864  bnj1452  31246  subfacp1lem1  31287  subfacp1lem5  31292  erdszelem4  31302  erdszelem8  31306  sconnpi1  31347  cvmscld  31381  cvmlift2lem6  31416  cvmlift2lem9  31419  cvmlift2lem11  31421  cvmlift2lem12  31422  mrsubvrs  31545  slerec  32048  neibastop2lem  32480  topjoin  32485  fnejoin2  32489  poimirlem3  33542  poimirlem9  33548  poimirlem28  33567  poimirlem32  33571  prdsbnd  33722  heiborlem8  33747  rrnequiv  33764  grpokerinj  33822  0idl  33954  prnc  33996  isfldidl  33997  lshpnel2N  34590  lsatfixedN  34614  lfl0f  34674  lkrlsp3  34709  elpaddatriN  35407  elpaddat  35408  elpadd2at  35410  pmodlem1  35450  osumcllem1N  35560  osumcllem2N  35561  osumcllem9N  35568  osumcllem10N  35569  pexmidlem6N  35579  pexmidlem7N  35580  dibss  36775  dochocsn  36987  dochsncom  36988  dochnel  36999  dihprrnlem1N  37030  dihprrnlem2  37031  djhlsmat  37033  dihsmsprn  37036  dvh4dimlem  37049  dvhdimlem  37050  dochsnnz  37056  dochsatshp  37057  dochsnshp  37059  dochexmid  37074  dochsnkr  37078  dochsnkr2cl  37080  dochfl1  37082  lcfl7lem  37105  lcfl6  37106  lcfl8  37108  lcfl9a  37111  lclkrlem2a  37113  lclkrlem2c  37115  lclkrlem2d  37116  lclkrlem2e  37117  lclkrlem2j  37122  lclkrlem2o  37127  lclkrlem2p  37128  lclkrlem2s  37131  lclkrlem2v  37134  lcfrlem14  37162  lcfrlem18  37166  lcfrlem19  37167  lcfrlem20  37168  lcfrlem23  37171  lcfrlem25  37173  lcdlkreqN  37228  mapdval4N  37238  mapdsn  37247  mapdhvmap  37375  hdmaprnlem4tN  37461  hdmapinvlem1  37527  hdmapinvlem2  37528  hdmapinvlem3  37529  hdmapinvlem4  37530  hdmapglem5  37531  hgmapvvlem3  37534  hdmapglem7a  37536  hdmapglem7b  37537  hdmapglem7  37538  hdmapoc  37540  elrfi  37574  cmpfiiin  37577  mzpcompact2lem  37631  dfac11  37949  pwssplit4  37976  rngunsnply  38060  flcidc  38061  acsfn1p  38086  proot1mul  38094  iocinico  38114  iunrelexp0  38311  frege81d  38356  k0004lem3  38764  binomcxplemnn0  38865  fsumsplit1  40122  islptre  40169  limciccioolb  40171  limcicciooub  40187  limcresiooub  40192  limcresioolb  40193  ioccncflimc  40416  icccncfext  40418  icocncflimc  40420  cncfiooicc  40425  dvnprodlem2  40480  dirkercncflem2  40639  dirkercncflem3  40640  fourierdlem48  40689  fourierdlem49  40690  fourierdlem79  40720  fourierdlem101  40742  sge0sup  40926  hoidmvlelem2  41131  hoiqssbl  41160  hspmbllem1  41161  hspmbllem2  41162  ovnovollem1  41191  fsumsplitsndif  41668  perfectALTVlem2  41956  1hegrlfgr  42038  gsumdifsndf  42469
  Copyright terms: Public domain W3C validator