Theorem snss 3886

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.

Step	Hyp	Ref	Expression
1		elsn 3789	. . . 4 |- ( x e. { A } <-> x = A )
2	1	imbi1i 316	. . 3 |- ( ( x e. { A } -> x e. B ) <-> ( x = A -> x e. B ) )
3	2	albii 1572	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3297	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3032	. 2 |- ( A e. B <-> A. x ( x = A -> x e. B ) )
7	3, 4, 6	3bitr4ri 270	1 |- ( A e. B <-> { A } C_ B )

Syntax hints:   -> wi 4   <-> wb 177   A.wal 1546   = wceq 1649   e. wcel 1721   _Vcvv 2916   C_ wss 3280   {csn 3774

This theorem is referenced by:  snssg  3892  prss  3912  tpss  3924  snelpw  4370  sspwb  4373  nnullss  4385  exss  4386  pwssun  4449  relsn  4938  fvimacnvi  5803  fvimacnv  5804  fvimacnvALT  5808  fnressn  5877  limensuci  7242  domunfican  7338  finsschain  7371  epfrs  7623  tc2  7637  tcsni  7638  cda1dif  8012  fpwwe2lem13  8473  wunfi  8552  uniwun  8571  un0mulcl  10210  nn0ssz  10258  xrinfmss  10844  hashbclem  11656  hashf1lem1  11659  hashf1lem2  11660  fsum2dlem  12509  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  incexclem  12571  ramcl2  13339  0ram  13343  strfv  13456  imasaddfnlem  13708  imasaddvallem  13709  acsfn1  13841  drsdirfi  14350  sylow2a  15208  gsumpt  15500  dprdfadd  15533  ablfac1eulem  15585  pgpfaclem1  15594  rsp1  16250  mplcoe1  16483  mplcoe2  16485  opnnei  17139  iscnp4  17281  cnpnei  17282  hausnei2  17371  fiuncmp  17421  llycmpkgen2  17535  1stckgen  17539  ptbasfi  17566  xkoccn  17604  xkoptsub  17639  ptcmpfi  17798  cnextcn  18051  tsmsid  18122  ustuqtop3  18226  utopreg  18235  prdsdsf  18350  prdsmet  18353  prdsbl  18474  fsumcn  18853  itgfsum  19671  dvmptfsum  19812  elply2  20068  elplyd  20074  ply1term  20076  ply0  20080  plymullem  20088  jensenlem1  20778  jensenlem2  20779  h1de2bi  23009  spansni  23012  cntnevol  24535  cvmlift2lem1  24942  cvmlift2lem12  24954  fprod2dlem  25257  dfon2lem7  25359  divrngidl  26528  isfldidl  26568  ispridlc  26570  acsfn1p  27375  frisusgranb  28101  pclfinclN  30432  osumcllem10N  30447  pexmidlem7N  30458

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

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 2391  df-cleq 2397  df-clel 2400  df-v 2918  df-in 3287  df-ss 3294  df-sn 3780