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

Theorem snss 3748
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, 5-Aug-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 3655 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 315 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1553 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3169 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2904 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 269 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684   _Vcvv 2788    C_ wss 3152   {csn 3640
This theorem is referenced by:  snssg  3754  prss  3769  tpss  3779  snelpw  4221  sspwb  4223  nnullss  4235  exss  4236  pwssun  4299  relsn  4790  fvimacnvi  5639  fvimacnv  5640  fvimacnvALT  5644  fnressn  5705  limensuci  7037  domunfican  7129  finsschain  7162  epfrs  7413  tc2  7427  tcsni  7428  cda1dif  7802  fpwwe2lem13  8264  wunfi  8343  uniwun  8362  un0mulcl  9998  nn0ssz  10044  xrinfmss  10628  hashbclem  11390  hashf1lem1  11393  hashf1lem2  11394  fsum2dlem  12233  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  incexclem  12295  ramcl2  13063  0ram  13067  strfv  13180  imasaddfnlem  13430  imasaddvallem  13431  acsfn1  13563  drsdirfi  14072  sylow2a  14930  gsumpt  15222  dprdfadd  15255  ablfac1eulem  15307  pgpfaclem1  15316  rsp1  15976  mplcoe1  16209  mplcoe2  16211  opnnei  16857  cnpnei  16993  hausnei2  17081  fiuncmp  17131  llycmpkgen2  17245  1stckgen  17249  ptbasfi  17276  xkoccn  17313  xkoptsub  17348  ptcmpfi  17504  tsmsid  17822  prdsdsf  17931  prdsmet  17934  prdsbl  18037  fsumcn  18374  itgfsum  19181  dvmptfsum  19322  elply2  19578  elplyd  19584  ply1term  19586  ply0  19590  plymullem  19598  jensenlem1  20281  jensenlem2  20282  h1de2bi  22133  spansni  22136  cntnevol  23175  cvmlift2lem1  23833  cvmlift2lem12  23845  dfon2lem7  24145  iscnp4  25563  phckle  26027  psckle  26028  smbkle  26043  pgapspf  26052  divrngidl  26653  isfldidl  26693  ispridlc  26695  acsfn1p  27507  pclfinclN  30139  osumcllem10N  30154  pexmidlem7N  30165
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-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790  df-in 3159  df-ss 3166  df-sn 3646
  Copyright terms: Public domain W3C validator