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

Theorem snssd 3760
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 3754 . . 3  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
31, 2syl 15 . 2  |-  ( ph  ->  ( A  e.  B  <->  { A }  C_  B
) )
41, 3mpbid 201 1  |-  ( ph  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1684    C_ wss 3152   {csn 3640
This theorem is referenced by:  frirr  4370  fr3nr  4571  sofld  5121  oeeui  6600  ecinxp  6734  xpdom3  6960  domunsn  7011  mapdom3  7033  isinf  7076  ac6sfi  7101  pwfilem  7150  finsschain  7162  ssfii  7172  marypha1lem  7186  unxpwdom2  7302  mapfien  7399  fseqenlem1  7651  axdc3lem4  8079  axdc4lem  8081  ttukeylem7  8142  fpwwe2lem13  8264  canthwe  8273  canthp1lem1  8274  wuncval2  8369  un0addcl  9997  un0mulcl  9998  fseq1p1m1  10857  hashbclem  11390  hashf1lem1  11393  fsumge1  12255  isumltss  12307  rpnnen2lem11  12503  bitsinv1  12633  phicl2  12836  vdwlem1  13028  vdwlem8  13035  vdwlem12  13039  vdwlem13  13040  0ram  13067  ramub1lem1  13073  ramub1lem2  13074  ramcl  13076  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasvscaf  13441  mrieqvlemd  13531  mreexmrid  13545  mreexexlem4d  13549  acsfiindd  14280  acsmapd  14281  gsumvallem2  14449  gsumress  14454  0subg  14642  cycsubg2cl  14655  odf1o1  14883  gex1  14902  sylow2alem1  14928  sylow2alem2  14929  lsm01  14980  lsm02  14981  lsmdisj  14990  lsmdisj2  14991  prmcyg  15180  gsumzadd  15204  gsumconst  15209  gsumpt  15222  gsumxp  15227  dmdprdd  15237  dprdfadd  15255  dprdres  15263  dprdz  15265  dprdsn  15271  dprddisj2  15274  dprd2da  15277  dprd2d2  15279  dmdprdsplit2lem  15280  dpjcntz  15287  dpjdisj  15288  dpjlsm  15289  dpjidcl  15293  ablfacrp  15301  ablfac1eu  15308  pgpfac1lem1  15309  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem5  15314  pgpfaclem2  15317  lsssn0  15705  lss0ss  15706  lsptpcl  15736  lspsnvsi  15761  lspun0  15768  lsmpr  15842  lsppr  15846  lspsntri  15850  lspsolvlem  15895  lspsolv  15896  lsppratlem1  15900  lsppratlem3  15902  lsppratlem4  15903  islbs3  15908  lbsextlem4  15914  rsp1  15976  lidlnz  15980  lidldvgen  16007  psrlidm  16148  psrridm  16149  mplmonmul  16208  mulgrhm2  16461  zndvds  16503  en2top  16723  rest0  16900  ordtrest  16932  cnconst2  17011  cnpdis  17021  ist1-2  17075  cnt1  17078  dishaus  17110  discmp  17125  cmpcld  17129  concompid  17157  dis2ndc  17186  dislly  17223  llycmpkgen2  17245  cmpkgen  17246  1stckgenlem  17248  1stckgen  17249  ptbasfi  17276  txdis  17326  txdis1cn  17329  txcmplem1  17335  xkohaus  17347  xkoptsub  17348  xkoinjcn  17381  pt1hmeo  17497  snfbas  17561  trnei  17587  isufil2  17603  ufileu  17614  filufint  17615  uffixsn  17620  ufildom1  17621  flimopn  17670  hausflim  17676  flimcf  17677  flimclslem  17679  flimsncls  17681  cnpflf2  17695  cnpflf  17696  fclsneii  17712  fclsfnflim  17722  fcfnei  17730  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  cldsubg  17793  snclseqg  17798  divstgphaus  17805  tsmsgsum  17821  tsmsid  17822  tgptsmscld  17833  tsmsxplem1  17835  tsmsxplem2  17836  prdsdsf  17931  prdsxmetlem  17932  prdsmet  17934  imasdsf1olem  17937  xpsdsval  17945  prdsbl  18037  prdsxmslem2  18075  idnghm  18252  icccmplem2  18328  metnrmlem2  18364  ioombl  18922  volivth  18962  itg11  19046  i1fmulclem  19057  itg2mulclem  19101  itgsplitioo  19192  limcvallem  19221  limcdif  19226  ellimc2  19227  limcflf  19231  limcmpt2  19234  limcres  19236  cnplimc  19237  limccnp  19241  limccnp2  19242  limcco  19243  dvreslem  19259  dvaddbr  19287  dvmulbr  19288  dvcmulf  19294  dvef  19327  dvivth  19357  lhop2  19362  lhop  19363  ply1remlem  19548  fta1blem  19554  ig1peu  19557  ig1pdvds  19562  plyco0  19574  elply2  19578  plyf  19580  elplyr  19583  elplyd  19584  ply1term  19586  ply0  19590  plyeq0lem  19592  plyeq0  19593  plypf1  19594  plyaddlem  19597  plymullem  19598  dgrlem  19611  coef2  19613  coeidlem  19619  plyco  19623  coemulhi  19635  plycj  19658  vieta1  19692  taylf  19740  radcnv0  19792  abelth  19817  rlimcnp  20260  xrlimcnp  20263  amgm  20285  wilthlem2  20307  basellem7  20324  basellem9  20326  ppiprm  20389  chtprm  20391  musumsum  20432  muinv  20433  logexprlim  20464  perfectlem2  20469  dchrhash  20510  rpvmasum2  20661  0oo  21367  sh0le  22019  esumsn  23437  subfacp1lem1  23710  subfacp1lem5  23715  erdszelem4  23725  erdszelem8  23729  sconpi1  23770  cvmscld  23804  cvmlift2lem6  23839  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  umgraex  23875  umgra1  23878  eupa0  23898  eupap1  23900  wfrlem15  24270  axlowdimlem7  24576  axlowdimlem10  24579  iscnp4  25563  tartarmap  25888  lineval12a  26084  comppfsc  26307  neibastop2lem  26309  topjoin  26314  fnejoin2  26318  prdsbnd  26517  heiborlem8  26542  rrnequiv  26559  grpokerinj  26575  0idl  26650  prnc  26692  isfldidl  26693  ralxpmap  26761  elrfi  26769  cmpfiiin  26772  mzpcompact2lem  26829  dfac11  27160  pwssplit1  27188  pwssplit4  27191  rngunsnply  27378  flcidc  27379  en2other2  27382  pmtrprfv  27396  acsfn1p  27507  proot1mul  27515  uslgra1  28118  usgra1  28119  uvtxnm1nbgra  28166  bnj1452  29082  lshpnel2N  29175  lsatfixedN  29199  lfl0f  29259  lkrlsp3  29294  elpaddatriN  29992  elpaddat  29993  elpadd2at  29995  pmodlem1  30035  osumcllem1N  30145  osumcllem2N  30146  osumcllem9N  30153  osumcllem10N  30154  pexmidlem6N  30164  pexmidlem7N  30165  dibss  31359  dochocsn  31571  dochsncom  31572  dochnel  31583  dihprrnlem1N  31614  dihprrnlem2  31615  djhlsmat  31617  dihsmsprn  31620  dvh4dimlem  31633  dvhdimlem  31634  dochsnnz  31640  dochsatshp  31641  dochsnshp  31643  dochexmid  31658  dochsnkr  31662  dochsnkr2cl  31664  dochfl1  31666  lcfl7lem  31689  lcfl6  31690  lcfl8  31692  lcfl9a  31695  lclkrlem2a  31697  lclkrlem2c  31699  lclkrlem2d  31700  lclkrlem2e  31701  lclkrlem2j  31706  lclkrlem2o  31711  lclkrlem2p  31712  lclkrlem2s  31715  lclkrlem2v  31718  lcfrlem14  31746  lcfrlem18  31750  lcfrlem19  31751  lcfrlem20  31752  lcfrlem23  31755  lcfrlem25  31757  lcdlkreqN  31812  mapdval4N  31822  mapdsn  31831  mapdhvmap  31959  hdmaprnlem4tN  32045  hdmapinvlem1  32111  hdmapinvlem2  32112  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem5  32115  hgmapvvlem3  32118  hdmapglem7a  32120  hdmapglem7b  32121  hdmapglem7  32122  hdmapoc  32124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-sn 3646
  Copyright terms: Public domain W3C validator