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

Theorem snss 3722
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 3629 . . . 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 3144 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2879 . 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 2763    C_ wss 3127   {csn 3614
This theorem is referenced by:  snssg  3728  prss  3743  tpss  3753  snelpw  4193  sspwb  4195  nnullss  4207  exss  4208  pwssun  4271  relsn  4778  fvimacnvi  5573  fvimacnv  5574  fvimacnvALT  5578  fnressn  5639  limensuci  7005  domunfican  7097  finsschain  7130  epfrs  7381  tc2  7395  tcsni  7396  cda1dif  7770  fpwwe2lem13  8232  wunfi  8311  uniwun  8330  un0mulcl  9966  nn0ssz  10012  xrinfmss  10595  hashbclem  11356  hashf1lem1  11359  hashf1lem2  11360  fsum2dlem  12199  fsumabs  12225  fsumrlim  12235  fsumo1  12236  fsumiun  12245  ramcl2  13026  0ram  13030  strfv  13143  imasaddfnlem  13393  imasaddvallem  13394  acsfn1  13526  drsdirfi  14035  sylow2a  14893  gsumpt  15185  dprdfadd  15218  ablfac1eulem  15270  pgpfaclem1  15279  rsp1  15939  mplcoe1  16172  mplcoe2  16174  opnnei  16820  cnpnei  16956  hausnei2  17044  fiuncmp  17094  llycmpkgen2  17208  1stckgen  17212  ptbasfi  17239  xkoccn  17276  xkoptsub  17311  ptcmpfi  17467  tsmsid  17785  prdsdsf  17894  prdsmet  17897  prdsbl  18000  fsumcn  18337  itgfsum  19144  dvmptfsum  19285  elply2  19541  elplyd  19547  ply1term  19549  ply0  19553  plymullem  19561  jensenlem1  20244  jensenlem2  20245  h1de2bi  22094  spansni  22097  cvmlift2lem1  23206  cvmlift2lem12  23218  dfon2lem7  23515  iscnp4  24931  phckle  25395  psckle  25396  smbkle  25411  pgapspf  25420  divrngidl  26021  isfldidl  26061  ispridlc  26063  acsfn1p  26875  pclfinclN  29389  osumcllem10N  29404  pexmidlem7N  29415
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 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-v 2765  df-in 3134  df-ss 3141  df-sn 3620
  Copyright terms: Public domain W3C validator