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

Theorem snss 4098
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, 21-Jun-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 3988 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 325 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1663 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3433 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 3188 . 2  |-  ( A  e.  B  <->  A. x
( x  =  A  ->  x  e.  B
) )
73, 4, 63bitr4ri 280 1  |-  ( A  e.  B  <->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186   A.wal 1405    = wceq 1407    e. wcel 1844   _Vcvv 3061    C_ wss 3416   {csn 3974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-v 3063  df-in 3423  df-ss 3430  df-sn 3975
This theorem is referenced by:  snssg  4107  prss  4128  tpss  4139  snelpw  4639  sspwb  4642  nnullss  4655  exss  4656  pwssun  4731  relsn  4929  fvimacnvi  5981  fvimacnv  5982  fvimacnvALT  5986  fnressn  6065  limensuci  7733  domunfican  7829  finsschain  7863  epfrs  8196  tc2  8207  tcsni  8208  cda1dif  8590  fpwwe2lem13  9052  wunfi  9131  uniwun  9150  un0mulcl  10873  nn0ssz  10928  xrinfmss  11556  hashbclem  12552  hashf1lem1  12555  hashf1lem2  12556  fsum2dlem  13738  fsumabs  13768  fsumrlim  13778  fsumo1  13779  fsumiun  13788  incexclem  13801  fprod2dlem  13938  ramcl2  14745  0ram  14749  strfv  14879  imasaddfnlem  15144  imasaddvallem  15145  acsfn1  15277  drsdirfi  15893  sylow2a  16965  gsumpt  17311  gsumptOLD  17312  dprdfadd  17382  dprdfaddOLD  17389  ablfac1eulem  17445  pgpfaclem1  17454  rsp1  18194  mplcoe1  18449  mplcoe5  18453  mplcoe2OLD  18455  mdetunilem9  19416  opnnei  19916  iscnp4  20059  cnpnei  20060  hausnei2  20149  fiuncmp  20199  llycmpkgen2  20345  1stckgen  20349  ptbasfi  20376  xkoccn  20414  xkoptsub  20449  ptcmpfi  20608  cnextcn  20861  tsmsid  20932  tsmsidOLD  20935  ustuqtop3  21040  utopreg  21049  prdsdsf  21164  prdsmet  21167  prdsbl  21288  fsumcn  21668  itgfsum  22527  dvmptfsum  22670  elply2  22887  elplyd  22893  ply1term  22895  ply0  22899  plymullem  22907  jensenlem1  23644  jensenlem2  23645  frisusgranb  25426  h1de2bi  26899  spansni  26902  gsumle  28234  gsumvsca1  28238  gsumvsca2  28239  ordtconlem1  28372  esum2dlem  28552  cntnevol  28689  oms0  28758  eulerpartgbij  28830  cvmlift2lem1  29612  cvmlift2lem12  29624  dfon2lem7  30021  bj-tagss  31116  divrngidl  31720  isfldidl  31760  ispridlc  31762  pclfinclN  32980  osumcllem10N  32995  pexmidlem7N  33006  acsfn1p  35525  fourierdlem62  37332
  Copyright terms: Public domain W3C validator