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

Theorem snss 3869
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 3772 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 316 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1572 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3280 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3015 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 270 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    = wceq 1649    e. wcel 1717   _Vcvv 2899    C_ wss 3263   {csn 3757
This theorem is referenced by:  snssg  3875  prss  3895  tpss  3907  snelpw  4351  sspwb  4354  nnullss  4366  exss  4367  pwssun  4430  relsn  4919  fvimacnvi  5783  fvimacnv  5784  fvimacnvALT  5788  fnressn  5857  limensuci  7219  domunfican  7315  finsschain  7348  epfrs  7600  tc2  7614  tcsni  7615  cda1dif  7989  fpwwe2lem13  8450  wunfi  8529  uniwun  8548  un0mulcl  10186  nn0ssz  10234  xrinfmss  10820  hashbclem  11628  hashf1lem1  11631  hashf1lem2  11632  fsum2dlem  12481  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  incexclem  12543  ramcl2  13311  0ram  13315  strfv  13428  imasaddfnlem  13680  imasaddvallem  13681  acsfn1  13813  drsdirfi  14322  sylow2a  15180  gsumpt  15472  dprdfadd  15505  ablfac1eulem  15557  pgpfaclem1  15566  rsp1  16222  mplcoe1  16455  mplcoe2  16457  opnnei  17107  iscnp4  17249  cnpnei  17250  hausnei2  17339  fiuncmp  17389  llycmpkgen2  17503  1stckgen  17507  ptbasfi  17534  xkoccn  17572  xkoptsub  17607  ptcmpfi  17766  cnextcn  18019  tsmsid  18090  ustuqtop3  18194  utopreg  18203  prdsdsf  18305  prdsmet  18308  prdsbl  18411  fsumcn  18771  itgfsum  19585  dvmptfsum  19726  elply2  19982  elplyd  19988  ply1term  19990  ply0  19994  plymullem  20002  jensenlem1  20692  jensenlem2  20693  h1de2bi  22904  spansni  22907  cntnevol  24376  cvmlift2lem1  24768  cvmlift2lem12  24780  dfon2lem7  25169  divrngidl  26329  isfldidl  26369  ispridlc  26371  acsfn1p  27176  frisusgranb  27750  pclfinclN  30064  osumcllem10N  30079  pexmidlem7N  30090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-v 2901  df-in 3270  df-ss 3277  df-sn 3763
  Copyright terms: Public domain W3C validator