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

Theorem snss 4109
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  |-  A  e. 
_V
Assertion
Ref Expression
snss  |-  ( A  e.  B  <->  { A }  C_  B )

Proof of Theorem snss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elsn 3994 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 331 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1702 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3433 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3187 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 286 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453    = wceq 1455    e. wcel 1898   _Vcvv 3057    C_ wss 3416   {csn 3980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059  df-in 3423  df-ss 3430  df-sn 3981
This theorem is referenced by:  snssg  4118  prss  4139  tpss  4150  snelpw  4663  sspwb  4666  nnullss  4679  exss  4680  pwssun  4762  relsn  4960  fvimacnvi  6024  fvimacnv  6025  fvimacnvALT  6029  fnressn  6105  limensuci  7779  domunfican  7875  finsschain  7912  epfrs  8246  tc2  8257  tcsni  8258  cda1dif  8637  fpwwe2lem13  9098  wunfi  9177  uniwun  9196  un0mulcl  10938  nn0ssz  10992  xrinfmss  11629  hashbclem  12654  hashf1lem1  12657  hashf1lem2  12658  fsum2dlem  13886  fsumabs  13916  fsumrlim  13926  fsumo1  13927  fsumiun  13936  incexclem  13949  fprod2dlem  14089  lcmfunsnlem  14669  lcmfun  14673  coprmprod  14733  coprmproddvdslem  14734  ramcl2  15028  ramcl2OLD  15029  0ram  15033  strfv  15212  imasaddfnlem  15489  imasaddvallem  15490  acsfn1  15622  drsdirfi  16238  sylow2a  17326  gsumpt  17649  dprdfadd  17708  ablfac1eulem  17760  pgpfaclem1  17769  rsp1  18503  mplcoe1  18744  mplcoe5  18747  mdetunilem9  19700  opnnei  20191  iscnp4  20334  cnpnei  20335  hausnei2  20424  fiuncmp  20474  llycmpkgen2  20620  1stckgen  20624  ptbasfi  20651  xkoccn  20689  xkoptsub  20724  ptcmpfi  20883  cnextcn  21137  tsmsid  21209  ustuqtop3  21313  utopreg  21322  prdsdsf  21437  prdsmet  21440  prdsbl  21561  fsumcn  21957  itgfsum  22840  dvmptfsum  22983  elply2  23206  elplyd  23212  ply1term  23214  ply0  23218  plymullem  23226  jensenlem1  23968  jensenlem2  23969  frisusgranb  25781  h1de2bi  27263  spansni  27266  gsumle  28593  gsumvsca1  28596  gsumvsca2  28597  ordtconlem1  28781  esum2dlem  28964  cntnevol  29101  oms0OLD  29179  eulerpartgbij  29255  cvmlift2lem1  30075  cvmlift2lem12  30087  dfon2lem7  30485  bj-tagss  31620  divrngidl  32307  isfldidl  32347  ispridlc  32349  pclfinclN  33561  osumcllem10N  33576  pexmidlem7N  33587  acsfn1p  36111  fourierdlem62  38133
  Copyright terms: Public domain W3C validator