Theorem snss 4139

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.

Step	Hyp	Ref	Expression
1		elsn 4028	. . . 4 |- ( x e. { A } <-> x = A )
2	1	imbi1i 325	. . 3 |- ( ( x e. { A } -> x e. B ) <-> ( x = A -> x e. B ) )
3	2	albii 1627	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3478	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3222	. 2 |- ( A e. B <-> A. x ( x = A -> x e. B ) )
7	3, 4, 6	3bitr4ri 278	1 |- ( A e. B <-> { A } C_ B )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1381   = wceq 1383   e. wcel 1804   _Vcvv 3095   C_ wss 3461   {csn 4014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-in 3468  df-ss 3475  df-sn 4015

This theorem is referenced by:  snssg  4148  prss  4169  tpss  4180  snelpw  4683  sspwb  4686  nnullss  4699  exss  4700  pwssun  4776  relsn  5096  fvimacnvi  5986  fvimacnv  5987  fvimacnvALT  5991  fnressn  6068  limensuci  7695  domunfican  7795  finsschain  7829  epfrs  8165  tc2  8176  tcsni  8177  cda1dif  8559  fpwwe2lem13  9023  wunfi  9102  uniwun  9121  un0mulcl  10837  nn0ssz  10892  xrinfmss  11512  hashbclem  12483  hashf1lem1  12486  hashf1lem2  12487  fsum2dlem  13567  fsumabs  13597  fsumrlim  13607  fsumo1  13608  fsumiun  13617  incexclem  13630  fprod2dlem  13766  ramcl2  14516  0ram  14520  strfv  14648  imasaddfnlem  14907  imasaddvallem  14908  acsfn1  15040  drsdirfi  15546  sylow2a  16618  gsumpt  16967  gsumptOLD  16968  dprdfadd  17039  dprdfaddOLD  17046  ablfac1eulem  17102  pgpfaclem1  17111  rsp1  17851  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  mdetunilem9  19100  opnnei  19599  iscnp4  19742  cnpnei  19743  hausnei2  19832  fiuncmp  19882  llycmpkgen2  20029  1stckgen  20033  ptbasfi  20060  xkoccn  20098  xkoptsub  20133  ptcmpfi  20292  cnextcn  20545  tsmsid  20616  tsmsidOLD  20619  ustuqtop3  20724  utopreg  20733  prdsdsf  20848  prdsmet  20851  prdsbl  20972  fsumcn  21352  itgfsum  22211  dvmptfsum  22354  elply2  22571  elplyd  22577  ply1term  22579  ply0  22583  plymullem  22591  jensenlem1  23294  jensenlem2  23295  frisusgranb  24975  h1de2bi  26450  spansni  26453  gsumle  27748  gsumvsca1  27751  gsumvsca2  27752  ordtconlem1  27884  cntnevol  28177  oms0  28244  eulerpartgbij  28289  cvmlift2lem1  28725  cvmlift2lem12  28737  dfon2lem7  29197  divrngidl  30401  isfldidl  30441  ispridlc  30443  acsfn1p  31124  fourierdlem62  31905  bj-tagss  34421  pclfinclN  35549  osumcllem10N  35564  pexmidlem7N  35575