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

Theorem snss 3652
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
StepHypRef Expression
1 elsn 3559 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 317 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1554 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3092 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2841 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 271 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532    = wceq 1619    e. wcel 1621   _Vcvv 2727    C_ wss 3078   {csn 3544
This theorem is referenced by:  snssg  3656  prss  3669  tpss  3679  snelpw  4115  sspwb  4117  nnullss  4128  exss  4129  pwssun  4192  relsn  4697  fvimacnvi  5491  fvimacnv  5492  fvimacnvALT  5496  fnressn  5557  limensuci  6922  domunfican  7014  finsschain  7046  epfrs  7297  tc2  7311  tcsni  7312  cda1dif  7686  fpwwe2lem13  8144  wunfi  8223  uniwun  8242  un0mulcl  9877  nn0ssz  9923  xrinfmss  10506  hashbclem  11267  hashf1lem1  11270  hashf1lem2  11271  fsum2dlem  12110  fsumabs  12136  fsumrlim  12146  fsumo1  12147  fsumiun  12156  ramcl2  12937  0ram  12941  strfv  13054  imasaddfnlem  13304  imasaddvallem  13305  acsfn1  13407  drsdirfi  13916  sylow2a  14765  gsumpt  15057  dprdfadd  15090  ablfac1eulem  15142  pgpfaclem1  15151  rsp1  15808  mplcoe1  16041  mplcoe2  16043  opnnei  16689  cnpnei  16825  hausnei2  16913  fiuncmp  16963  llycmpkgen2  17077  1stckgen  17081  ptbasfi  17108  xkoccn  17145  xkoptsub  17180  ptcmpfi  17336  tsmsid  17654  prdsdsf  17763  prdsmet  17766  prdsbl  17869  fsumcn  18206  itgfsum  19013  dvmptfsum  19154  elply2  19410  elplyd  19416  ply1term  19418  ply0  19422  plymullem  19430  jensenlem1  20113  jensenlem2  20114  h1de2bi  21963  spansni  21966  cvmlift2lem1  23004  cvmlift2lem12  23016  dfon2lem7  23313  iscnp4  24729  phckle  25193  psckle  25194  smbkle  25209  pgapspf  25218  divrngidl  25819  isfldidl  25859  ispridlc  25861  acsfn1p  26673  pclfinclN  28828  osumcllem10N  28843  pexmidlem7N  28854
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-v 2729  df-in 3085  df-ss 3089  df-sn 3550
  Copyright terms: Public domain W3C validator