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

Theorem snssd 4160
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 4148 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 16 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 210 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1804    C_ wss 3461   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-in 3468  df-ss 3475  df-sn 4015
This theorem is referenced by:  frirr  4846  sofld  5445  fr3nr  6600  oeeui  7253  ecinxp  7388  ralxpmap  7470  xpdom3  7617  domunsn  7669  mapdom3  7691  isinf  7735  ac6sfi  7766  pwfilem  7816  finsschain  7829  ssfii  7881  marypha1lem  7895  unxpwdom2  8017  mapfienOLD  8141  en2other2  8390  fseqenlem1  8408  axdc3lem4  8836  axdc4lem  8838  ttukeylem7  8898  fpwwe2lem13  9023  canthwe  9032  canthp1lem1  9033  wuncval2  9128  un0addcl  10836  un0mulcl  10837  fseq1p1m1  11763  hashbclem  12483  hashf1lem1  12486  fsumge1  13593  incexclem  13630  isumltss  13642  rpnnen2lem11  13940  bitsinv1  14074  phicl2  14280  vdwlem1  14481  vdwlem8  14488  vdwlem12  14492  vdwlem13  14493  0ram  14520  ramub1lem1  14526  ramub1lem2  14527  ramcl  14529  imasaddfnlem  14907  imasaddflem  14909  imasvscafn  14916  imasvscaf  14918  mrieqvlemd  15008  mreexmrid  15022  mreexexlem4d  15026  acsfiindd  15786  acsmapd  15787  gsumress  15882  gsumvallem2  15982  0subg  16205  cycsubg2cl  16218  pmtrprfv  16457  odf1o1  16571  gex1  16590  sylow2alem1  16616  sylow2alem2  16617  lsm01  16668  lsm02  16669  lsmdisj  16678  lsmdisj2  16679  prmcyg  16875  gsumzadd  16914  gsumzaddOLD  16916  gsumconst  16933  gsumdifsnd  16966  gsumpt  16967  gsumptOLD  16968  gsumxp  16983  gsumxpOLD  16985  dmdprdd  17009  dprdfadd  17039  dprdfaddOLD  17046  dprdres  17054  dprdz  17056  dprdsn  17062  dprddisj2  17066  dprddisj2OLD  17067  dprd2da  17070  dprd2d2  17072  dmdprdsplit2lem  17073  dpjcntz  17080  dpjdisj  17081  dpjlsm  17082  dpjidcl  17086  dpjidclOLD  17093  ablfacrp  17096  ablfac1eu  17103  pgpfac1lem1  17104  pgpfac1lem3a  17106  pgpfac1lem3  17107  pgpfac1lem5  17109  pgpfaclem2  17112  kerf1hrm  17371  lsssn0  17573  lss0ss  17574  lsptpcl  17604  lspsnvsi  17629  lspun0  17636  pwssplit1  17684  lsmpr  17714  lsppr  17718  lspsntri  17722  lspsolvlem  17767  lspsolv  17768  lsppratlem1  17772  lsppratlem3  17774  lsppratlem4  17775  islbs3  17780  lbsextlem4  17786  rsp1  17851  lidlnz  17855  lidldvgen  17882  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  mplmonmul  18105  mulgrhm2  18511  mulgrhm2OLD  18514  zndvds  18566  mdetdiaglem  19078  mdetrlin  19082  mdetrsca  19083  mdetrsca2  19084  mdetrlin2  19087  mdetunilem5  19096  mdetunilem9  19100  mdetmul  19103  en2top  19465  rest0  19648  ordtrest  19681  iscnp4  19742  cnconst2  19762  cnpdis  19772  ist1-2  19826  cnt1  19829  dishaus  19861  discmp  19876  cmpcld  19880  concompid  19910  dis2ndc  19939  dislly  19976  dissnref  20007  comppfsc  20011  llycmpkgen2  20029  cmpkgen  20030  1stckgenlem  20032  1stckgen  20033  ptbasfi  20060  txdis  20111  txdis1cn  20114  txcmplem1  20120  xkohaus  20132  xkoptsub  20133  xkoinjcn  20166  pt1hmeo  20285  snfbas  20345  trnei  20371  isufil2  20387  ufileu  20398  filufint  20399  uffixsn  20404  ufildom1  20405  flimopn  20454  hausflim  20460  flimcf  20461  flimclslem  20463  flimsncls  20465  cnpflf2  20479  cnpflf  20480  fclsneii  20496  fclsfnflim  20506  fcfnei  20514  alexsubALTlem3  20527  alexsubALTlem4  20528  ptcmplem2  20531  cldsubg  20587  snclseqg  20592  qustgphaus  20599  tsmsgsum  20615  tsmsid  20616  tsmsgsumOLD  20618  tsmsidOLD  20619  tgptsmscld  20631  tsmsxplem1  20633  tsmsxplem2  20634  ust0  20700  ustuqtop1  20722  neipcfilu  20777  prdsdsf  20848  prdsxmetlem  20849  prdsmet  20851  imasdsf1olem  20854  xpsdsval  20862  prdsbl  20972  prdsxmslem2  21010  idnghm  21228  icccmplem2  21306  metnrmlem2  21342  ioombl  21953  volivth  21994  itg11  22076  i1fmulclem  22087  itg2mulclem  22131  itgsplitioo  22222  limcvallem  22253  limcdif  22258  ellimc2  22259  limcflf  22263  limcmpt2  22266  limcres  22268  cnplimc  22269  limccnp  22273  limccnp2  22274  limcco  22275  dvreslem  22291  dvaddbr  22319  dvmulbr  22320  dvcmulf  22326  dvef  22359  dvivth  22389  lhop2  22394  lhop  22395  ply1remlem  22541  fta1blem  22547  ig1peu  22550  ig1pdvds  22555  plyco0  22567  elply2  22571  plyf  22573  elplyr  22576  elplyd  22577  ply1term  22579  ply0  22583  plyeq0lem  22585  plyeq0  22586  plypf1  22587  plyaddlem  22590  plymullem  22591  dgrlem  22604  coef2  22606  coeidlem  22612  plyco  22616  coemulhi  22629  plycj  22652  vieta1  22686  taylf  22734  radcnv0  22789  abelth  22814  rlimcnp  23273  xrlimcnp  23276  amgm  23298  wilthlem2  23321  basellem7  23338  basellem9  23340  ppiprm  23403  chtprm  23405  musumsum  23446  muinv  23447  logexprlim  23478  perfectlem2  23483  dchrhash  23524  rpvmasum2  23675  axlowdimlem7  24229  axlowdimlem10  24232  umgraex  24301  umgra1  24304  uslgra1  24350  usgra1  24351  uvtxnm1nbgra  24472  constr1trl  24568  eupa0  24952  eupap1  24954  0oo  25682  sh0le  26336  qtopt1  27816  locfinref  27822  ordtrestNEW  27881  esumsn  28050  eulerpartlems  28277  eulerpartlemgc  28279  eulerpartlemgh  28295  eulerpartlemgs2  28297  plymulx0  28482  subfacp1lem1  28601  subfacp1lem5  28606  erdszelem4  28616  erdszelem8  28620  sconpi1  28662  cvmscld  28696  cvmlift2lem6  28731  cvmlift2lem9  28734  cvmlift2lem11  28736  cvmlift2lem12  28737  mrsubvrs  28860  wfrlem15  29333  neibastop2lem  30154  topjoin  30159  fnejoin2  30163  prdsbnd  30265  heiborlem8  30290  rrnequiv  30307  grpokerinj  30323  0idl  30398  prnc  30440  isfldidl  30441  elrfi  30602  cmpfiiin  30605  mzpcompact2lem  30660  dfac11  30984  pwssplit4  31011  rngunsnply  31098  flcidc  31099  acsfn1p  31124  proot1mul  31132  iocinico  31155  fsumsplit1  31527  islptre  31579  limciccioolb  31581  limcicciooub  31597  limcresiooub  31602  limcresioolb  31603  ioccncflimc  31642  icccncfext  31644  icocncflimc  31646  cncfiooicc  31651  dvnprodlem2  31698  dirkercncflem2  31840  dirkercncflem3  31841  fourierdlem48  31891  fourierdlem49  31892  fourierdlem79  31922  fourierdlem101  31944  fsumsplitsndif  32300  gsumdifsndf  32823  bnj1452  33976  lshpnel2N  34585  lsatfixedN  34609  lfl0f  34669  lkrlsp3  34704  elpaddatriN  35402  elpaddat  35403  elpadd2at  35405  pmodlem1  35445  osumcllem1N  35555  osumcllem2N  35556  osumcllem9N  35563  osumcllem10N  35564  pexmidlem6N  35574  pexmidlem7N  35575  dibss  36771  dochocsn  36983  dochsncom  36984  dochnel  36995  dihprrnlem1N  37026  dihprrnlem2  37027  djhlsmat  37029  dihsmsprn  37032  dvh4dimlem  37045  dvhdimlem  37046  dochsnnz  37052  dochsatshp  37053  dochsnshp  37055  dochexmid  37070  dochsnkr  37074  dochsnkr2cl  37076  dochfl1  37078  lcfl7lem  37101  lcfl6  37102  lcfl8  37104  lcfl9a  37107  lclkrlem2a  37109  lclkrlem2c  37111  lclkrlem2d  37112  lclkrlem2e  37113  lclkrlem2j  37118  lclkrlem2o  37123  lclkrlem2p  37124  lclkrlem2s  37127  lclkrlem2v  37130  lcfrlem14  37158  lcfrlem18  37162  lcfrlem19  37163  lcfrlem20  37164  lcfrlem23  37167  lcfrlem25  37169  lcdlkreqN  37224  mapdval4N  37234  mapdsn  37243  mapdhvmap  37371  hdmaprnlem4tN  37457  hdmapinvlem1  37523  hdmapinvlem2  37524  hdmapinvlem3  37525  hdmapinvlem4  37526  hdmapglem5  37527  hgmapvvlem3  37530  hdmapglem7a  37532  hdmapglem7b  37533  hdmapglem7  37534  hdmapoc  37536
  Copyright terms: Public domain W3C validator