Theorem snss 4741

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4740). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
snss.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snss	⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Proof of Theorem snss

Step	Hyp	Ref	Expression
1		snss.1	. 2 ⊢ 𝐴 ∈ V
2		snssg 4740	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-sn 4581

This theorem is referenced by:  tpss  4793  sspwb  5397  nnullss  5410  exss  5411  pwssun  5516  fvimacnvi  6997  fvimacnv  6998  fvimacnvALT  7002  fnressn  7103  limensuci  9081  domunfican  9222  finsschain  9259  epfrs  9640  tc2  9649  tcsni  9650  dju1dif  10083  fpwwe2lem12  10553  wunfi  10632  uniwun  10651  un0mulcl  12435  nn0ssz  12511  xrinfmss  13225  hashbclem  14375  hashf1lem1  14378  hashf1lem2  14379  fsum2dlem  15693  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  incexclem  15759  fprod2dlem  15903  lcmfunsnlem  16568  lcmfun  16572  coprmprod  16588  coprmproddvdslem  16589  ramcl2  16944  0ram  16948  strfv  17130  imasaddfnlem  17449  imasaddvallem  17450  acsfn1  17584  drsdirfi  18228  sylow2a  19548  gsumpt  19891  dprdfadd  19951  ablfac1eulem  20003  pgpfaclem1  20012  gsumle  20074  acsfn1p  20732  rsp1  21192  pzriprnglem4  21439  mplcoe1  21992  mplcoe5  21995  mdetunilem9  22564  opnnei  23064  iscnp4  23207  cnpnei  23208  hausnei2  23297  fiuncmp  23348  llycmpkgen2  23494  1stckgen  23498  ptbasfi  23525  xkoccn  23563  xkoptsub  23598  ptcmpfi  23757  cnextcn  24011  tsmsid  24084  ustuqtop3  24187  utopreg  24196  prdsdsf  24311  prdsmet  24314  prdsbl  24435  fsumcn  24817  itgfsum  25784  dvmptfsum  25935  elply2  26157  elplyd  26163  ply1term  26165  ply0  26169  plymullem  26177  jensenlem1  26953  jensenlem2  26954  frcond3  30344  h1de2bi  31629  spansni  31632  gsumvsca1  33308  gsumvsca2  33309  1fldgenq  33404  unitprodclb  33470  mxidlirredi  33552  extdg1id  33823  ordtconnlem1  34081  cntnevol  34385  eulerpartgbij  34529  breprexpnat  34791  cvmlift2lem1  35496  cvmlift2lem12  35508  dfon2lem7  35981  bj-tagss  37181  lindsenlbs  37816  matunitlindflem1  37817  divrngidl  38229  isfldidl  38269  ispridlc  38271  pclfinclN  40210  osumcllem10N  40225  pexmidlem7N  40236  clsk1indlem4  44285  clsk1indlem1  44286  fourierdlem62  46412  nthrucw  47130