Theorem snss 4106

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 3998	. . . 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 1611	. 2 |- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
4		dfss2 3452	. 2 |- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
5		snss.1	. . 3 |- A e. _V
6	5	clel2 3201	. 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 1368   = wceq 1370   e. wcel 1758   _Vcvv 3076   C_ wss 3435   {csn 3984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3078  df-in 3442  df-ss 3449  df-sn 3985

This theorem is referenced by:  snssg  4114  prss  4134  tpss  4145  snelpw  4645  sspwb  4648  nnullss  4661  exss  4662  pwssun  4734  relsn  5050  fvimacnvi  5925  fvimacnv  5926  fvimacnvALT  5930  fnressn  6002  limensuci  7596  domunfican  7694  finsschain  7728  epfrs  8061  tc2  8072  tcsni  8073  cda1dif  8455  fpwwe2lem13  8919  wunfi  8998  uniwun  9017  un0mulcl  10724  nn0ssz  10777  xrinfmss  11382  hashbclem  12322  hashf1lem1  12325  hashf1lem2  12326  fsum2dlem  13354  fsumabs  13381  fsumrlim  13391  fsumo1  13392  fsumiun  13401  incexclem  13416  ramcl2  14194  0ram  14198  strfv  14325  imasaddfnlem  14584  imasaddvallem  14585  acsfn1  14717  drsdirfi  15226  sylow2a  16238  gsumpt  16575  gsumptOLD  16576  dprdfadd  16631  dprdfaddOLD  16638  ablfac1eulem  16694  pgpfaclem1  16703  rsp1  17428  mplcoe1  17667  mplcoe5  17671  mplcoe2OLD  17673  mdetunilem9  18557  opnnei  18855  iscnp4  18998  cnpnei  18999  hausnei2  19088  fiuncmp  19138  llycmpkgen2  19254  1stckgen  19258  ptbasfi  19285  xkoccn  19323  xkoptsub  19358  ptcmpfi  19517  cnextcn  19770  tsmsid  19841  tsmsidOLD  19844  ustuqtop3  19949  utopreg  19958  prdsdsf  20073  prdsmet  20076  prdsbl  20197  fsumcn  20577  itgfsum  21436  dvmptfsum  21579  elply2  21796  elplyd  21802  ply1term  21804  ply0  21808  plymullem  21816  jensenlem1  22512  jensenlem2  22513  h1de2bi  25108  spansni  25111  gsumle  26390  gsumvsca1  26395  gsumvsca2  26396  ordtconlem1  26498  cntnevol  26786  oms0  26853  eulerpartgbij  26898  plymulx0  27091  cvmlift2lem1  27334  cvmlift2lem12  27346  fprod2dlem  27634  dfon2lem7  27745  divrngidl  28975  isfldidl  29015  ispridlc  29017  acsfn1p  29703  frisusgranb  30736  bj-tagss  32790  pclfinclN  33917  osumcllem10N  33932  pexmidlem7N  33943