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

Theorem snss 3918
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 3821 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 316 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1575 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3329 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3064 . 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 1549    = wceq 1652    e. wcel 1725   _Vcvv 2948    C_ wss 3312   {csn 3806
This theorem is referenced by:  snssg  3924  prss  3944  tpss  3956  snelpw  4402  sspwb  4405  nnullss  4417  exss  4418  pwssun  4481  relsn  4971  fvimacnvi  5836  fvimacnv  5837  fvimacnvALT  5841  fnressn  5910  limensuci  7275  domunfican  7371  finsschain  7405  epfrs  7659  tc2  7673  tcsni  7674  cda1dif  8048  fpwwe2lem13  8509  wunfi  8588  uniwun  8607  un0mulcl  10246  nn0ssz  10294  xrinfmss  10880  hashbclem  11693  hashf1lem1  11696  hashf1lem2  11697  fsum2dlem  12546  fsumabs  12572  fsumrlim  12582  fsumo1  12583  fsumiun  12592  incexclem  12608  ramcl2  13376  0ram  13380  strfv  13493  imasaddfnlem  13745  imasaddvallem  13746  acsfn1  13878  drsdirfi  14387  sylow2a  15245  gsumpt  15537  dprdfadd  15570  ablfac1eulem  15622  pgpfaclem1  15631  rsp1  16287  mplcoe1  16520  mplcoe2  16522  opnnei  17176  iscnp4  17319  cnpnei  17320  hausnei2  17409  fiuncmp  17459  llycmpkgen2  17574  1stckgen  17578  ptbasfi  17605  xkoccn  17643  xkoptsub  17678  ptcmpfi  17837  cnextcn  18090  tsmsid  18161  ustuqtop3  18265  utopreg  18274  prdsdsf  18389  prdsmet  18392  prdsbl  18513  fsumcn  18892  itgfsum  19710  dvmptfsum  19851  elply2  20107  elplyd  20113  ply1term  20115  ply0  20119  plymullem  20127  jensenlem1  20817  jensenlem2  20818  h1de2bi  23048  spansni  23051  cntnevol  24574  cvmlift2lem1  24981  cvmlift2lem12  24993  fprod2dlem  25296  dfon2lem7  25408  divrngidl  26629  isfldidl  26669  ispridlc  26671  acsfn1p  27475  frisusgranb  28324  pclfinclN  30684  osumcllem10N  30699  pexmidlem7N  30710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950  df-in 3319  df-ss 3326  df-sn 3812
  Copyright terms: Public domain W3C validator