Theorem snss 3994

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 3886	. . . 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 1610	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3340	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3091	. 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 1367   = wceq 1369   e. wcel 1756   _Vcvv 2967   C_ wss 3323   {csn 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2969  df-in 3330  df-ss 3337  df-sn 3873

This theorem is referenced by:  snssg  4002  prss  4022  tpss  4033  snelpw  4533  sspwb  4536  nnullss  4549  exss  4550  pwssun  4622  relsn  4938  fvimacnvi  5812  fvimacnv  5813  fvimacnvALT  5817  fnressn  5889  limensuci  7479  domunfican  7576  finsschain  7610  epfrs  7943  tc2  7954  tcsni  7955  cda1dif  8337  fpwwe2lem13  8801  wunfi  8880  uniwun  8899  un0mulcl  10606  nn0ssz  10659  xrinfmss  11264  hashbclem  12197  hashf1lem1  12200  hashf1lem2  12201  fsum2dlem  13229  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  incexclem  13291  ramcl2  14069  0ram  14073  strfv  14200  imasaddfnlem  14458  imasaddvallem  14459  acsfn1  14591  drsdirfi  15100  sylow2a  16109  gsumpt  16444  gsumptOLD  16445  dprdfadd  16500  dprdfaddOLD  16507  ablfac1eulem  16563  pgpfaclem1  16572  rsp1  17286  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  mdetunilem9  18406  opnnei  18704  iscnp4  18847  cnpnei  18848  hausnei2  18937  fiuncmp  18987  llycmpkgen2  19103  1stckgen  19107  ptbasfi  19134  xkoccn  19172  xkoptsub  19207  ptcmpfi  19366  cnextcn  19619  tsmsid  19690  tsmsidOLD  19693  ustuqtop3  19798  utopreg  19807  prdsdsf  19922  prdsmet  19925  prdsbl  20046  fsumcn  20426  itgfsum  21284  dvmptfsum  21427  elply2  21644  elplyd  21650  ply1term  21652  ply0  21656  plymullem  21664  jensenlem1  22360  jensenlem2  22361  h1de2bi  24929  spansni  24932  gsumle  26218  gsumvsca1  26223  gsumvsca2  26224  ordtconlem1  26327  cntnevol  26615  oms0  26683  eulerpartgbij  26728  plymulx0  26921  cvmlift2lem1  27164  cvmlift2lem12  27176  fprod2dlem  27464  dfon2lem7  27575  divrngidl  28802  isfldidl  28842  ispridlc  28844  acsfn1p  29530  frisusgranb  30563  bj-tagss  32397  pclfinclN  33511  osumcllem10N  33526  pexmidlem7N  33537