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

Theorem snssd 3858
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 3847 . . 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 1715    C_ wss 3238   {csn 3729
This theorem is referenced by:  frirr  4473  fr3nr  4674  sofld  5224  oeeui  6742  ecinxp  6876  xpdom3  7103  domunsn  7154  mapdom3  7176  isinf  7219  ac6sfi  7248  pwfilem  7297  finsschain  7309  ssfii  7319  marypha1lem  7333  unxpwdom2  7449  mapfien  7546  fseqenlem1  7798  axdc3lem4  8226  axdc4lem  8228  ttukeylem7  8289  fpwwe2lem13  8411  canthwe  8420  canthp1lem1  8421  wuncval2  8516  un0addcl  10146  un0mulcl  10147  fseq1p1m1  11012  hashbclem  11588  hashf1lem1  11591  fsumge1  12463  isumltss  12515  rpnnen2lem11  12711  bitsinv1  12841  phicl2  13044  vdwlem1  13236  vdwlem8  13243  vdwlem12  13247  vdwlem13  13248  0ram  13275  ramub1lem1  13281  ramub1lem2  13282  ramcl  13284  imasaddfnlem  13640  imasaddflem  13642  imasvscafn  13649  imasvscaf  13651  mrieqvlemd  13741  mreexmrid  13755  mreexexlem4d  13759  acsfiindd  14490  acsmapd  14491  gsumvallem2  14659  gsumress  14664  0subg  14852  cycsubg2cl  14865  odf1o1  15093  gex1  15112  sylow2alem1  15138  sylow2alem2  15139  lsm01  15190  lsm02  15191  lsmdisj  15200  lsmdisj2  15201  prmcyg  15390  gsumzadd  15414  gsumconst  15419  gsumpt  15432  gsumxp  15437  dmdprdd  15447  dprdfadd  15465  dprdres  15473  dprdz  15475  dprdsn  15481  dprddisj2  15484  dprd2da  15487  dprd2d2  15489  dmdprdsplit2lem  15490  dpjcntz  15497  dpjdisj  15498  dpjlsm  15499  dpjidcl  15503  ablfacrp  15511  ablfac1eu  15518  pgpfac1lem1  15519  pgpfac1lem3a  15521  pgpfac1lem3  15522  pgpfac1lem5  15524  pgpfaclem2  15527  lsssn0  15915  lss0ss  15916  lsptpcl  15946  lspsnvsi  15971  lspun0  15978  lsmpr  16052  lsppr  16056  lspsntri  16060  lspsolvlem  16105  lspsolv  16106  lsppratlem1  16110  lsppratlem3  16112  lsppratlem4  16113  islbs3  16118  lbsextlem4  16124  rsp1  16186  lidlnz  16190  lidldvgen  16217  psrlidm  16358  psrridm  16359  mplmonmul  16418  mulgrhm2  16678  zndvds  16720  en2top  16940  rest0  17117  ordtrest  17149  cnconst2  17228  cnpdis  17238  ist1-2  17292  cnt1  17295  dishaus  17327  discmp  17342  cmpcld  17346  concompid  17374  dis2ndc  17403  dislly  17440  llycmpkgen2  17462  cmpkgen  17463  1stckgenlem  17465  1stckgen  17466  ptbasfi  17493  txdis  17543  txdis1cn  17546  txcmplem1  17552  xkohaus  17564  xkoptsub  17565  xkoinjcn  17598  pt1hmeo  17714  snfbas  17774  trnei  17800  isufil2  17816  ufileu  17827  filufint  17828  uffixsn  17833  ufildom1  17834  flimopn  17883  hausflim  17889  flimcf  17890  flimclslem  17892  flimsncls  17894  cnpflf2  17908  cnpflf  17909  fclsneii  17925  fclsfnflim  17935  fcfnei  17943  alexsubALTlem3  17956  alexsubALTlem4  17957  ptcmplem2  17960  cldsubg  18006  snclseqg  18011  divstgphaus  18018  tsmsgsum  18034  tsmsid  18035  tgptsmscld  18046  tsmsxplem1  18048  tsmsxplem2  18049  prdsdsf  18144  prdsxmetlem  18145  prdsmet  18147  imasdsf1olem  18150  xpsdsval  18158  prdsbl  18250  prdsxmslem2  18288  idnghm  18465  icccmplem2  18542  metnrmlem2  18578  ioombl  19137  volivth  19177  itg11  19261  i1fmulclem  19272  itg2mulclem  19316  itgsplitioo  19407  limcvallem  19436  limcdif  19441  ellimc2  19442  limcflf  19446  limcmpt2  19449  limcres  19451  cnplimc  19452  limccnp  19456  limccnp2  19457  limcco  19458  dvreslem  19474  dvaddbr  19502  dvmulbr  19503  dvcmulf  19509  dvef  19542  dvivth  19572  lhop2  19577  lhop  19578  ply1remlem  19763  fta1blem  19769  ig1peu  19772  ig1pdvds  19777  plyco0  19789  elply2  19793  plyf  19795  elplyr  19798  elplyd  19799  ply1term  19801  ply0  19805  plyeq0lem  19807  plyeq0  19808  plypf1  19809  plyaddlem  19812  plymullem  19813  dgrlem  19826  coef2  19828  coeidlem  19834  plyco  19838  coemulhi  19850  plycj  19873  vieta1  19907  taylf  19955  radcnv0  20010  abelth  20035  rlimcnp  20482  xrlimcnp  20485  amgm  20507  wilthlem2  20530  basellem7  20547  basellem9  20549  ppiprm  20612  chtprm  20614  musumsum  20655  muinv  20656  logexprlim  20687  perfectlem2  20692  dchrhash  20733  rpvmasum2  20884  umgraex  21036  umgra1  21039  uslgra1  21070  usgra1  21071  uvtxnm1nbgra  21173  eupa0  21207  eupap1  21209  0oo  21801  sh0le  22453  kerf1hrm  23748  iscnp4  23767  ustuqtop1  23865  esumsn  24042  subfacp1lem1  24434  subfacp1lem5  24439  erdszelem4  24449  erdszelem8  24453  sconpi1  24494  cvmscld  24528  cvmlift2lem6  24563  cvmlift2lem9  24566  cvmlift2lem11  24568  cvmlift2lem12  24569  wfrlem15  25096  axlowdimlem7  25403  axlowdimlem10  25406  comppfsc  25899  neibastop2lem  25901  topjoin  25906  fnejoin2  25910  prdsbnd  26108  heiborlem8  26133  rrnequiv  26150  grpokerinj  26166  0idl  26241  prnc  26283  isfldidl  26284  ralxpmap  26352  elrfi  26360  cmpfiiin  26363  mzpcompact2lem  26420  dfac11  26751  pwssplit1  26779  pwssplit4  26782  rngunsnply  26969  flcidc  26970  en2other2  26973  pmtrprfv  26987  acsfn1p  27098  proot1mul  27106  constr1trl  27735  bnj1452  28834  lshpnel2N  29234  lsatfixedN  29258  lfl0f  29318  lkrlsp3  29353  elpaddatriN  30051  elpaddat  30052  elpadd2at  30054  pmodlem1  30094  osumcllem1N  30204  osumcllem2N  30205  osumcllem9N  30212  osumcllem10N  30213  pexmidlem6N  30223  pexmidlem7N  30224  dibss  31418  dochocsn  31630  dochsncom  31631  dochnel  31642  dihprrnlem1N  31673  dihprrnlem2  31674  djhlsmat  31676  dihsmsprn  31679  dvh4dimlem  31692  dvhdimlem  31693  dochsnnz  31699  dochsatshp  31700  dochsnshp  31702  dochexmid  31717  dochsnkr  31721  dochsnkr2cl  31723  dochfl1  31725  lcfl7lem  31748  lcfl6  31749  lcfl8  31751  lcfl9a  31754  lclkrlem2a  31756  lclkrlem2c  31758  lclkrlem2d  31759  lclkrlem2e  31760  lclkrlem2j  31765  lclkrlem2o  31770  lclkrlem2p  31771  lclkrlem2s  31774  lclkrlem2v  31777  lcfrlem14  31805  lcfrlem18  31809  lcfrlem19  31810  lcfrlem20  31811  lcfrlem23  31814  lcfrlem25  31816  lcdlkreqN  31871  mapdval4N  31881  mapdsn  31890  mapdhvmap  32018  hdmaprnlem4tN  32104  hdmapinvlem1  32170  hdmapinvlem2  32171  hdmapinvlem3  32172  hdmapinvlem4  32173  hdmapglem5  32174  hgmapvvlem3  32177  hdmapglem7a  32179  hdmapglem7b  32180  hdmapglem7  32181  hdmapoc  32183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-sn 3735
  Copyright terms: Public domain W3C validator