Theorem snss 4151

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 4041	. . . 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 1620	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3493	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3240	. 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 1377   = wceq 1379   e. wcel 1767   _Vcvv 3113   C_ wss 3476   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115  df-in 3483  df-ss 3490  df-sn 4028

This theorem is referenced by:  snssg  4160  prss  4181  tpss  4192  snelpw  4693  sspwb  4696  nnullss  4709  exss  4710  pwssun  4786  relsn  5106  fvimacnvi  5995  fvimacnv  5996  fvimacnvALT  6000  fnressn  6073  limensuci  7693  domunfican  7793  finsschain  7827  epfrs  8162  tc2  8173  tcsni  8174  cda1dif  8556  fpwwe2lem13  9020  wunfi  9099  uniwun  9118  un0mulcl  10830  nn0ssz  10885  xrinfmss  11501  hashbclem  12467  hashf1lem1  12470  hashf1lem2  12471  fsum2dlem  13548  fsumabs  13578  fsumrlim  13588  fsumo1  13589  fsumiun  13598  incexclem  13611  ramcl2  14393  0ram  14397  strfv  14524  imasaddfnlem  14783  imasaddvallem  14784  acsfn1  14916  drsdirfi  15425  sylow2a  16445  gsumpt  16791  gsumptOLD  16792  dprdfadd  16862  dprdfaddOLD  16869  ablfac1eulem  16925  pgpfaclem1  16934  rsp1  17671  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  mdetunilem9  18917  opnnei  19415  iscnp4  19558  cnpnei  19559  hausnei2  19648  fiuncmp  19698  llycmpkgen2  19814  1stckgen  19818  ptbasfi  19845  xkoccn  19883  xkoptsub  19918  ptcmpfi  20077  cnextcn  20330  tsmsid  20401  tsmsidOLD  20404  ustuqtop3  20509  utopreg  20518  prdsdsf  20633  prdsmet  20636  prdsbl  20757  fsumcn  21137  itgfsum  21996  dvmptfsum  22139  elply2  22356  elplyd  22362  ply1term  22364  ply0  22368  plymullem  22376  jensenlem1  23072  jensenlem2  23073  frisusgranb  24701  h1de2bi  26176  spansni  26179  gsumle  27461  gsumvsca1  27464  gsumvsca2  27465  ordtconlem1  27570  cntnevol  27867  oms0  27934  eulerpartgbij  27979  plymulx0  28172  cvmlift2lem1  28415  cvmlift2lem12  28427  fprod2dlem  28715  dfon2lem7  28826  divrngidl  30056  isfldidl  30096  ispridlc  30098  acsfn1p  30781  fourierdlem62  31497  fourierdlem79  31514  bj-tagss  33637  pclfinclN  34764  osumcllem10N  34779  pexmidlem7N  34790