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

Theorem snss 4154
Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
snss.1
Assertion
Ref Expression
snss

Proof of Theorem snss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elsn 4043 . . . 4
21imbi1i 325 . . 3
32albii 1640 . 2
4 dfss2 3492 . 2
5 snss.1 . . 3
65clel2 3236 . 2
73, 4, 63bitr4ri 278 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818   cvv 3109  C_wss 3475  {csn 4029
This theorem is referenced by:  snssg  4163  prss  4184  tpss  4195  snelpw  4698  sspwb  4701  nnullss  4714  exss  4715  pwssun  4791  relsn  5111  fvimacnvi  6001  fvimacnv  6002  fvimacnvALT  6006  fnressn  6083  limensuci  7713  domunfican  7813  finsschain  7847  epfrs  8183  tc2  8194  tcsni  8195  cda1dif  8577  fpwwe2lem13  9041  wunfi  9120  uniwun  9139  un0mulcl  10855  nn0ssz  10910  xrinfmss  11530  hashbclem  12501  hashf1lem1  12504  hashf1lem2  12505  fsum2dlem  13585  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  incexclem  13648  fprod2dlem  13784  ramcl2  14534  0ram  14538  strfv  14666  imasaddfnlem  14925  imasaddvallem  14926  acsfn1  15058  drsdirfi  15567  sylow2a  16639  gsumpt  16988  gsumptOLD  16989  dprdfadd  17060  dprdfaddOLD  17067  ablfac1eulem  17123  pgpfaclem1  17132  rsp1  17872  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mdetunilem9  19122  opnnei  19621  iscnp4  19764  cnpnei  19765  hausnei2  19854  fiuncmp  19904  llycmpkgen2  20051  1stckgen  20055  ptbasfi  20082  xkoccn  20120  xkoptsub  20155  ptcmpfi  20314  cnextcn  20567  tsmsid  20638  tsmsidOLD  20641  ustuqtop3  20746  utopreg  20755  prdsdsf  20870  prdsmet  20873  prdsbl  20994  fsumcn  21374  itgfsum  22233  dvmptfsum  22376  elply2  22593  elplyd  22599  ply1term  22601  ply0  22605  plymullem  22613  jensenlem1  23316  jensenlem2  23317  frisusgranb  24997  h1de2bi  26472  spansni  26475  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  ordtconlem1  27906  cntnevol  28199  oms0  28266  eulerpartgbij  28311  cvmlift2lem1  28747  cvmlift2lem12  28759  dfon2lem7  29221  divrngidl  30425  isfldidl  30465  ispridlc  30467  acsfn1p  31148  fourierdlem62  31951  bj-tagss  34538  pclfinclN  35674  osumcllem10N  35689  pexmidlem7N  35700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-sn 4030
  Copyright terms: Public domain W3C validator