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

Theorem snss 4124
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 4012 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 326 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1685 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3453 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3207 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 281 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    = wceq 1437    e. wcel 1872   _Vcvv 3080    C_ wss 3436   {csn 3998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3082  df-in 3443  df-ss 3450  df-sn 3999
This theorem is referenced by:  snssg  4133  prss  4154  tpss  4165  snelpw  4667  sspwb  4670  nnullss  4683  exss  4684  pwssun  4759  relsn  4957  fvimacnvi  6011  fvimacnv  6012  fvimacnvALT  6016  fnressn  6091  limensuci  7757  domunfican  7853  finsschain  7890  epfrs  8223  tc2  8234  tcsni  8235  cda1dif  8613  fpwwe2lem13  9074  wunfi  9153  uniwun  9172  un0mulcl  10911  nn0ssz  10965  xrinfmss  11602  hashbclem  12619  hashf1lem1  12622  hashf1lem2  12623  fsum2dlem  13830  fsumabs  13860  fsumrlim  13870  fsumo1  13871  fsumiun  13880  incexclem  13893  fprod2dlem  14033  lcmfunsnlem  14613  lcmfun  14617  coprmprod  14677  coprmproddvdslem  14678  ramcl2  14972  ramcl2OLD  14973  0ram  14977  strfv  15156  imasaddfnlem  15433  imasaddvallem  15434  acsfn1  15566  drsdirfi  16182  sylow2a  17270  gsumpt  17593  dprdfadd  17652  ablfac1eulem  17704  pgpfaclem1  17713  rsp1  18447  mplcoe1  18688  mplcoe5  18691  mdetunilem9  19643  opnnei  20134  iscnp4  20277  cnpnei  20278  hausnei2  20367  fiuncmp  20417  llycmpkgen2  20563  1stckgen  20567  ptbasfi  20594  xkoccn  20632  xkoptsub  20667  ptcmpfi  20826  cnextcn  21080  tsmsid  21152  ustuqtop3  21256  utopreg  21265  prdsdsf  21380  prdsmet  21383  prdsbl  21504  fsumcn  21900  itgfsum  22782  dvmptfsum  22925  elply2  23148  elplyd  23154  ply1term  23156  ply0  23160  plymullem  23168  jensenlem1  23910  jensenlem2  23911  frisusgranb  25723  h1de2bi  27205  spansni  27208  gsumle  28549  gsumvsca1  28553  gsumvsca2  28554  ordtconlem1  28738  esum2dlem  28921  cntnevol  29058  oms0OLD  29137  eulerpartgbij  29213  cvmlift2lem1  30033  cvmlift2lem12  30045  dfon2lem7  30442  bj-tagss  31542  divrngidl  32225  isfldidl  32265  ispridlc  32267  pclfinclN  33484  osumcllem10N  33499  pexmidlem7N  33510  acsfn1p  36035  fourierdlem62  37972
  Copyright terms: Public domain W3C validator