Theorem snss 3987

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 3879	. . . 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 1613	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3333	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3085	. 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 1360   = wceq 1362   e. wcel 1755   _Vcvv 2962   C_ wss 3316   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-in 3323  df-ss 3330  df-sn 3866

This theorem is referenced by:  snssg  3995  prss  4015  tpss  4026  snelpw  4526  sspwb  4529  nnullss  4542  exss  4543  pwssun  4614  relsn  4930  fvimacnvi  5805  fvimacnv  5806  fvimacnvALT  5810  fnressn  5881  limensuci  7475  domunfican  7572  finsschain  7606  epfrs  7939  tc2  7950  tcsni  7951  cda1dif  8333  fpwwe2lem13  8796  wunfi  8875  uniwun  8894  un0mulcl  10601  nn0ssz  10654  xrinfmss  11259  hashbclem  12188  hashf1lem1  12191  hashf1lem2  12192  fsum2dlem  13220  fsumabs  13246  fsumrlim  13256  fsumo1  13257  fsumiun  13266  incexclem  13281  ramcl2  14059  0ram  14063  strfv  14190  imasaddfnlem  14448  imasaddvallem  14449  acsfn1  14581  drsdirfi  15090  sylow2a  16097  gsumpt  16428  gsumptOLD  16429  dprdfadd  16483  dprdfaddOLD  16490  ablfac1eulem  16546  pgpfaclem1  16555  rsp1  17227  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  mdetunilem9  18267  opnnei  18565  iscnp4  18708  cnpnei  18709  hausnei2  18798  fiuncmp  18848  llycmpkgen2  18964  1stckgen  18968  ptbasfi  18995  xkoccn  19033  xkoptsub  19068  ptcmpfi  19227  cnextcn  19480  tsmsid  19551  tsmsidOLD  19554  ustuqtop3  19659  utopreg  19668  prdsdsf  19783  prdsmet  19786  prdsbl  19907  fsumcn  20287  itgfsum  21145  dvmptfsum  21288  elply2  21548  elplyd  21554  ply1term  21556  ply0  21560  plymullem  21568  jensenlem1  22264  jensenlem2  22265  h1de2bi  24779  spansni  24782  gsumle  26097  gsumvsca1  26103  gsumvsca2  26104  ordtconlem1  26207  cntnevol  26495  eulerpartgbij  26602  plymulx0  26795  cvmlift2lem1  27038  cvmlift2lem12  27050  fprod2dlem  27337  dfon2lem7  27448  divrngidl  28669  isfldidl  28709  ispridlc  28711  acsfn1p  29398  frisusgranb  30432  bj-tagss  32053  pclfinclN  33164  osumcllem10N  33179  pexmidlem7N  33190