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

Theorem snss 3927
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 3830 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 317 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1576 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3338 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3073 . 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 4    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726   _Vcvv 2957    C_ wss 3321   {csn 3815
This theorem is referenced by:  snssg  3933  prss  3953  tpss  3965  snelpw  4411  sspwb  4414  nnullss  4426  exss  4427  pwssun  4490  relsn  4980  fvimacnvi  5845  fvimacnv  5846  fvimacnvALT  5850  fnressn  5919  limensuci  7284  domunfican  7380  finsschain  7414  epfrs  7668  tc2  7682  tcsni  7683  cda1dif  8057  fpwwe2lem13  8518  wunfi  8597  uniwun  8616  un0mulcl  10255  nn0ssz  10303  xrinfmss  10889  hashbclem  11702  hashf1lem1  11705  hashf1lem2  11706  fsum2dlem  12555  fsumabs  12581  fsumrlim  12591  fsumo1  12592  fsumiun  12601  incexclem  12617  ramcl2  13385  0ram  13389  strfv  13502  imasaddfnlem  13754  imasaddvallem  13755  acsfn1  13887  drsdirfi  14396  sylow2a  15254  gsumpt  15546  dprdfadd  15579  ablfac1eulem  15631  pgpfaclem1  15640  rsp1  16296  mplcoe1  16529  mplcoe2  16531  opnnei  17185  iscnp4  17328  cnpnei  17329  hausnei2  17418  fiuncmp  17468  llycmpkgen2  17583  1stckgen  17587  ptbasfi  17614  xkoccn  17652  xkoptsub  17687  ptcmpfi  17846  cnextcn  18099  tsmsid  18170  ustuqtop3  18274  utopreg  18283  prdsdsf  18398  prdsmet  18401  prdsbl  18522  fsumcn  18901  itgfsum  19719  dvmptfsum  19860  elply2  20116  elplyd  20122  ply1term  20124  ply0  20128  plymullem  20136  jensenlem1  20826  jensenlem2  20827  h1de2bi  23057  spansni  23060  cntnevol  24583  cvmlift2lem1  24990  cvmlift2lem12  25002  fprod2dlem  25305  dfon2lem7  25417  divrngidl  26639  isfldidl  26679  ispridlc  26681  acsfn1p  27485  frisusgranb  28388  pclfinclN  30748  osumcllem10N  30763  pexmidlem7N  30774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-v 2959  df-in 3328  df-ss 3335  df-sn 3821
  Copyright terms: Public domain W3C validator