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

Theorem snssd 4129
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  |-  ( ph  ->  A  e.  B )
Assertion
Ref Expression
snssd  |-  ( ph  ->  { A }  C_  B )

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2  |-  ( ph  ->  A  e.  B )
2 snssg 4117 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 215 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    e. wcel 1897    C_ wss 3415   {csn 3979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-in 3422  df-ss 3429  df-sn 3980
This theorem is referenced by:  frirr  4829  sofld  5302  fsnex  6205  fr3nr  6632  wfrlem15  7075  oeeui  7328  ecinxp  7463  ralxpmap  7546  xpdom3  7695  domunsn  7747  mapdom3  7769  isinf  7810  ac6sfi  7840  pwfilem  7893  finsschain  7906  ssfii  7958  marypha1lem  7972  unxpwdom2  8128  en2other2  8465  fseqenlem1  8480  axdc3lem4  8908  axdc4lem  8910  ttukeylem7  8970  fpwwe2lem13  9092  canthwe  9101  canthp1lem1  9102  wuncval2  9197  un0addcl  10931  un0mulcl  10932  fseq1p1m1  11896  hashbclem  12647  hashf1lem1  12650  fsumge1  13905  incexclem  13942  isumltss  13954  rpnnen2lem11  14325  bitsinv1  14464  lcmfunsnlem2  14661  lcmfass  14667  phicl2  14764  vdwlem1  14979  vdwlem8  14986  vdwlem12  14990  vdwlem13  14991  0ram  15026  ramub1lem1  15032  ramub1lem2  15033  ramcl  15035  imasaddfnlem  15482  imasaddflem  15484  imasvscafn  15491  imasvscaf  15493  mrieqvlemd  15583  mreexmrid  15597  mreexexlem4d  15601  acsfiindd  16471  acsmapd  16472  gsumress  16567  gsumvallem2  16667  0subg  16890  cycsubg2cl  16903  pmtrprfv  17142  odf1o1  17269  gex1  17291  sylow2alem1  17317  sylow2alem2  17318  lsm01  17369  lsm02  17370  lsmdisj  17379  lsmdisj2  17380  prmcyg  17576  gsumzadd  17603  gsumconst  17615  gsumdifsnd  17641  gsumpt  17642  gsumxp  17656  dmdprdd  17679  dprdfadd  17701  dprdres  17709  dprdz  17711  dprdsn  17717  dprddisj2  17720  dprd2da  17723  dprd2d2  17725  dmdprdsplit2lem  17726  dpjcntz  17733  dpjdisj  17734  dpjlsm  17735  dpjidcl  17739  ablfacrp  17747  ablfac1eu  17754  pgpfac1lem1  17755  pgpfac1lem3a  17757  pgpfac1lem3  17758  pgpfac1lem5  17760  pgpfaclem2  17763  kerf1hrm  18019  lsssn0  18219  lss0ss  18220  lsptpcl  18250  lspsnvsi  18275  lspun0  18282  pwssplit1  18330  lsmpr  18360  lsppr  18364  lspsntri  18368  lspsolvlem  18413  lspsolv  18414  lsppratlem1  18418  lsppratlem3  18420  lsppratlem4  18421  islbs3  18426  lbsextlem4  18432  rsp1  18496  lidlnz  18500  lidldvgen  18527  psrlidm  18675  psrridm  18676  mplmonmul  18736  mulgrhm2  19118  zndvds  19168  mdetdiaglem  19671  mdetrlin  19675  mdetrsca  19676  mdetrsca2  19677  mdetrlin2  19680  mdetunilem5  19689  mdetunilem9  19693  mdetmul  19696  en2top  20049  rest0  20233  ordtrest  20266  iscnp4  20327  cnconst2  20347  cnpdis  20357  ist1-2  20411  cnt1  20414  dishaus  20446  discmp  20461  cmpcld  20465  concompid  20494  dis2ndc  20523  dislly  20560  dissnref  20591  comppfsc  20595  llycmpkgen2  20613  cmpkgen  20614  1stckgenlem  20616  1stckgen  20617  ptbasfi  20644  txdis  20695  txdis1cn  20698  txcmplem1  20704  xkohaus  20716  xkoptsub  20717  xkoinjcn  20750  pt1hmeo  20869  snfbas  20929  trnei  20955  isufil2  20971  ufileu  20982  filufint  20983  uffixsn  20988  ufildom1  20989  flimopn  21038  hausflim  21044  flimcf  21045  flimclslem  21047  flimsncls  21049  cnpflf2  21063  cnpflf  21064  fclsneii  21080  fclsfnflim  21090  fcfnei  21098  flfcntr  21106  alexsubALTlem3  21112  alexsubALTlem4  21113  ptcmplem2  21116  cldsubg  21173  snclseqg  21178  qustgphaus  21185  tsmsgsum  21201  tsmsid  21202  tgptsmscld  21213  tsmsxplem1  21215  tsmsxplem2  21216  ust0  21282  ustuqtop1  21304  neipcfilu  21359  prdsdsf  21430  prdsxmetlem  21431  prdsmet  21433  imasdsf1olem  21436  xpsdsval  21444  prdsbl  21554  prdsxmslem2  21592  idnghm  21812  icccmplem2  21889  metnrmlem2  21925  metnrmlem2OLD  21940  ioombl  22566  volivth  22613  itg11  22697  i1fmulclem  22708  itg2mulclem  22752  itgsplitioo  22843  limcvallem  22874  limcdif  22879  ellimc2  22880  limcflf  22884  limcmpt2  22887  limcres  22889  cnplimc  22890  limccnp  22894  limccnp2  22895  limcco  22896  dvreslem  22912  dvaddbr  22940  dvmulbr  22941  dvcmulf  22947  dvef  22980  dvivth  23010  lhop2  23015  lhop  23016  ply1remlem  23161  fta1blem  23167  ig1peu  23170  ig1peuOLD  23171  ig1pdvds  23176  ig1pdvdsOLD  23182  plyco0  23194  elply2  23198  plyf  23200  elplyr  23203  elplyd  23204  ply1term  23206  ply0  23210  plyeq0lem  23212  plyeq0  23213  plypf1  23214  plyaddlem  23217  plymullem  23218  dgrlem  23231  coef2  23233  coeidlem  23239  plyco  23243  coemulhi  23256  plycj  23279  vieta1  23313  taylf  23364  radcnv0  23419  abelth  23444  rlimcnp  23939  xrlimcnp  23942  amgm  23964  wilthlem2  24042  basellem7  24061  basellem9  24063  ppiprm  24126  chtprm  24128  musumsum  24169  muinv  24170  logexprlim  24201  perfectlem2  24206  dchrhash  24247  rpvmasum2  24398  axlowdimlem7  25026  axlowdimlem10  25029  umgraex  25098  umgra1  25101  uslgra1  25147  usgra1  25148  uvtxnm1nbgra  25270  constr1trl  25366  eupa0  25750  eupap1  25752  0oo  26478  sh0le  27141  disjiunel  28254  qtopt1  28710  locfinref  28716  ordtrestNEW  28775  esumsnf  28933  rossros  29050  oms0  29173  carsggect  29198  eulerpartlems  29241  eulerpartlemgc  29243  eulerpartlemgh  29259  eulerpartlemgs2  29261  plymulx0  29484  bnj1452  29909  subfacp1lem1  29950  subfacp1lem5  29955  erdszelem4  29965  erdszelem8  29969  sconpi1  30010  cvmscld  30044  cvmlift2lem6  30079  cvmlift2lem9  30082  cvmlift2lem11  30084  cvmlift2lem12  30085  mrsubvrs  30208  neibastop2lem  31064  topjoin  31069  fnejoin2  31073  poimirlem3  31987  poimirlem9  31993  poimirlem28  32012  poimirlem32  32016  prdsbnd  32169  heiborlem8  32194  rrnequiv  32211  grpokerinj  32227  0idl  32302  prnc  32344  isfldidl  32345  lshpnel2N  32595  lsatfixedN  32619  lfl0f  32679  lkrlsp3  32714  elpaddatriN  33412  elpaddat  33413  elpadd2at  33415  pmodlem1  33455  osumcllem1N  33565  osumcllem2N  33566  osumcllem9N  33573  osumcllem10N  33574  pexmidlem6N  33584  pexmidlem7N  33585  dibss  34781  dochocsn  34993  dochsncom  34994  dochnel  35005  dihprrnlem1N  35036  dihprrnlem2  35037  djhlsmat  35039  dihsmsprn  35042  dvh4dimlem  35055  dvhdimlem  35056  dochsnnz  35062  dochsatshp  35063  dochsnshp  35065  dochexmid  35080  dochsnkr  35084  dochsnkr2cl  35086  dochfl1  35088  lcfl7lem  35111  lcfl6  35112  lcfl8  35114  lcfl9a  35117  lclkrlem2a  35119  lclkrlem2c  35121  lclkrlem2d  35122  lclkrlem2e  35123  lclkrlem2j  35128  lclkrlem2o  35133  lclkrlem2p  35134  lclkrlem2s  35137  lclkrlem2v  35140  lcfrlem14  35168  lcfrlem18  35172  lcfrlem19  35173  lcfrlem20  35174  lcfrlem23  35177  lcfrlem25  35179  lcdlkreqN  35234  mapdval4N  35244  mapdsn  35253  mapdhvmap  35381  hdmaprnlem4tN  35467  hdmapinvlem1  35533  hdmapinvlem2  35534  hdmapinvlem3  35535  hdmapinvlem4  35536  hdmapglem5  35537  hgmapvvlem3  35540  hdmapglem7a  35542  hdmapglem7b  35543  hdmapglem7  35544  hdmapoc  35546  elrfi  35580  cmpfiiin  35583  mzpcompact2lem  35637  dfac11  35964  pwssplit4  35991  rngunsnply  36083  flcidc  36084  acsfn1p  36109  proot1mul  36117  iocinico  36140  iunrelexp0  36338  frege81d  36383  binomcxplemnn0  36741  fsumsplit1  37688  islptre  37736  limciccioolb  37738  limcicciooub  37754  limcresiooub  37760  limcresioolb  37761  ioccncflimc  37800  icccncfext  37802  icocncflimc  37804  cncfiooicc  37809  dvnprodlem2  37859  dirkercncflem2  38003  dirkercncflem3  38004  fourierdlem48  38055  fourierdlem49  38056  fourierdlem79  38086  fourierdlem101  38108  sge0sup  38270  hoidmvlelem2  38455  hoiqssbl  38484  hspmbllem1  38485  hspmbllem2  38486  perfectALTVlem2  38881  fsumsplitsndif  39137  upgrex  39230  upgr1elem  39247  uvtxanm1nbgr  39526  umgr2v2e  39611  gsumdifsndf  40419
  Copyright terms: Public domain W3C validator