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

Theorem snss 3749
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 3656 . . . 4  |-  ( x  e.  { A }  <->  x  =  A )
21imbi1i 315 . . 3  |-  ( ( x  e.  { A }  ->  x  e.  B
)  <->  ( x  =  A  ->  x  e.  B ) )
32albii 1553 . 2  |-  ( A. x ( x  e. 
{ A }  ->  x  e.  B )  <->  A. x
( x  =  A  ->  x  e.  B
) )
4 dfss2 3170 . 2  |-  ( { A }  C_  B  <->  A. x ( x  e. 
{ A }  ->  x  e.  B ) )
5 snss.1 . . 3  |-  A  e. 
_V
65clel2 2905 . 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 1527    = wceq 1623    e. wcel 1685   _Vcvv 2789    C_ wss 3153   {csn 3641
This theorem is referenced by:  snssg  3755  prss  3770  tpss  3780  snelpw  4220  sspwb  4222  nnullss  4234  exss  4235  pwssun  4298  relsn  4789  fvimacnvi  5601  fvimacnv  5602  fvimacnvALT  5606  fnressn  5667  limensuci  7033  domunfican  7125  finsschain  7158  epfrs  7409  tc2  7423  tcsni  7424  cda1dif  7798  fpwwe2lem13  8260  wunfi  8339  uniwun  8358  un0mulcl  9994  nn0ssz  10040  xrinfmss  10624  hashbclem  11386  hashf1lem1  11389  hashf1lem2  11390  fsum2dlem  12229  fsumabs  12255  fsumrlim  12265  fsumo1  12266  fsumiun  12275  incexclem  12291  ramcl2  13059  0ram  13063  strfv  13176  imasaddfnlem  13426  imasaddvallem  13427  acsfn1  13559  drsdirfi  14068  sylow2a  14926  gsumpt  15218  dprdfadd  15251  ablfac1eulem  15303  pgpfaclem1  15312  rsp1  15972  mplcoe1  16205  mplcoe2  16207  opnnei  16853  cnpnei  16989  hausnei2  17077  fiuncmp  17127  llycmpkgen2  17241  1stckgen  17245  ptbasfi  17272  xkoccn  17309  xkoptsub  17344  ptcmpfi  17500  tsmsid  17818  prdsdsf  17927  prdsmet  17930  prdsbl  18033  fsumcn  18370  itgfsum  19177  dvmptfsum  19318  elply2  19574  elplyd  19580  ply1term  19582  ply0  19586  plymullem  19594  jensenlem1  20277  jensenlem2  20278  h1de2bi  22129  spansni  22132  cvmlift2lem1  23240  cvmlift2lem12  23252  dfon2lem7  23549  iscnp4  24974  phckle  25438  psckle  25439  smbkle  25454  pgapspf  25463  divrngidl  26064  isfldidl  26104  ispridlc  26106  acsfn1p  26918  pclfinclN  29418  osumcllem10N  29433  pexmidlem7N  29444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-v 2791  df-in 3160  df-ss 3167  df-sn 3647
  Copyright terms: Public domain W3C validator