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

Theorem snss 3761
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 3668 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 315 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1556 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3182 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2917 . 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 1530    = wceq 1632    e. wcel 1696   _Vcvv 2801    C_ wss 3165   {csn 3653
This theorem is referenced by:  snssg  3767  prss  3785  tpss  3795  snelpw  4237  sspwb  4239  nnullss  4251  exss  4252  pwssun  4315  relsn  4806  fvimacnvi  5655  fvimacnv  5656  fvimacnvALT  5660  fnressn  5721  limensuci  7053  domunfican  7145  finsschain  7178  epfrs  7429  tc2  7443  tcsni  7444  cda1dif  7818  fpwwe2lem13  8280  wunfi  8359  uniwun  8378  un0mulcl  10014  nn0ssz  10060  xrinfmss  10644  hashbclem  11406  hashf1lem1  11409  hashf1lem2  11410  fsum2dlem  12249  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  incexclem  12311  ramcl2  13079  0ram  13083  strfv  13196  imasaddfnlem  13446  imasaddvallem  13447  acsfn1  13579  drsdirfi  14088  sylow2a  14946  gsumpt  15238  dprdfadd  15271  ablfac1eulem  15323  pgpfaclem1  15332  rsp1  15992  mplcoe1  16225  mplcoe2  16227  opnnei  16873  cnpnei  17009  hausnei2  17097  fiuncmp  17147  llycmpkgen2  17261  1stckgen  17265  ptbasfi  17292  xkoccn  17329  xkoptsub  17364  ptcmpfi  17520  tsmsid  17838  prdsdsf  17947  prdsmet  17950  prdsbl  18053  fsumcn  18390  itgfsum  19197  dvmptfsum  19338  elply2  19594  elplyd  19600  ply1term  19602  ply0  19606  plymullem  19614  jensenlem1  20297  jensenlem2  20298  h1de2bi  22149  spansni  22152  cntnevol  23191  cvmlift2lem1  23848  cvmlift2lem12  23860  dfon2lem7  24216  iscnp4  25666  phckle  26130  psckle  26131  smbkle  26146  pgapspf  26155  divrngidl  26756  isfldidl  26796  ispridlc  26798  acsfn1p  27610  pclfinclN  30761  osumcllem10N  30776  pexmidlem7N  30787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-v 2803  df-in 3172  df-ss 3179  df-sn 3659
  Copyright terms: Public domain W3C validator