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

Theorem snss 3750
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 3657 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 315 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1555 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3171 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2906 . 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 1529    = wceq 1625    e. wcel 1686   _Vcvv 2790    C_ wss 3154   {csn 3642
This theorem is referenced by:  snssg  3756  prss  3771  tpss  3781  snelpw  4223  sspwb  4225  nnullss  4237  exss  4238  pwssun  4301  relsn  4792  fvimacnvi  5641  fvimacnv  5642  fvimacnvALT  5646  fnressn  5707  limensuci  7039  domunfican  7131  finsschain  7164  epfrs  7415  tc2  7429  tcsni  7430  cda1dif  7804  fpwwe2lem13  8266  wunfi  8345  uniwun  8364  un0mulcl  10000  nn0ssz  10046  xrinfmss  10630  hashbclem  11392  hashf1lem1  11395  hashf1lem2  11396  fsum2dlem  12235  fsumabs  12261  fsumrlim  12271  fsumo1  12272  fsumiun  12281  incexclem  12297  ramcl2  13065  0ram  13069  strfv  13182  imasaddfnlem  13432  imasaddvallem  13433  acsfn1  13565  drsdirfi  14074  sylow2a  14932  gsumpt  15224  dprdfadd  15257  ablfac1eulem  15309  pgpfaclem1  15318  rsp1  15978  mplcoe1  16211  mplcoe2  16213  opnnei  16859  cnpnei  16995  hausnei2  17083  fiuncmp  17133  llycmpkgen2  17247  1stckgen  17251  ptbasfi  17278  xkoccn  17315  xkoptsub  17350  ptcmpfi  17506  tsmsid  17824  prdsdsf  17933  prdsmet  17936  prdsbl  18039  fsumcn  18376  itgfsum  19183  dvmptfsum  19324  elply2  19580  elplyd  19586  ply1term  19588  ply0  19592  plymullem  19600  jensenlem1  20283  jensenlem2  20284  h1de2bi  22135  spansni  22138  cntnevol  23177  cvmlift2lem1  23835  cvmlift2lem12  23847  dfon2lem7  24147  iscnp4  25574  phckle  26038  psckle  26039  smbkle  26054  pgapspf  26063  divrngidl  26664  isfldidl  26704  ispridlc  26706  acsfn1p  27518  pclfinclN  30212  osumcllem10N  30227  pexmidlem7N  30238
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-v 2792  df-in 3161  df-ss 3168  df-sn 3648
  Copyright terms: Public domain W3C validator