Theorem snss 4718

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4717). 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 4717	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Vcvv 3494   ⊆ wss 3936  {csn 4567

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-sn 4568

This theorem is referenced by:  tpss  4768  snelpw  5338  sspwb  5342  nnullss  5354  exss  5355  pwssun  5456  fvimacnvi  6822  fvimacnv  6823  fvimacnvALT  6827  fnressn  6920  limensuci  8693  domunfican  8791  finsschain  8831  epfrs  9173  tc2  9184  tcsni  9185  dju1dif  9598  fpwwe2lem13  10064  wunfi  10143  uniwun  10162  un0mulcl  11932  nn0ssz  12004  xrinfmss  12704  hashbclem  13811  hashf1lem1  13814  hashf1lem2  13815  fsum2dlem  15125  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  incexclem  15191  fprod2dlem  15334  lcmfunsnlem  15985  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  ramcl2  16352  0ram  16356  strfv  16531  imasaddfnlem  16801  imasaddvallem  16802  acsfn1  16932  drsdirfi  17548  sylow2a  18744  gsumpt  19082  dprdfadd  19142  ablfac1eulem  19194  pgpfaclem1  19203  acsfn1p  19578  rsp1  19997  mplcoe1  20246  mplcoe5  20249  mdetunilem9  21229  opnnei  21728  iscnp4  21871  cnpnei  21872  hausnei2  21961  fiuncmp  22012  llycmpkgen2  22158  1stckgen  22162  ptbasfi  22189  xkoccn  22227  xkoptsub  22262  ptcmpfi  22421  cnextcn  22675  tsmsid  22748  ustuqtop3  22852  utopreg  22861  prdsdsf  22977  prdsmet  22980  prdsbl  23101  fsumcn  23478  itgfsum  24427  dvmptfsum  24572  elply2  24786  elplyd  24792  ply1term  24794  ply0  24798  plymullem  24806  jensenlem1  25564  jensenlem2  25565  frcond3  28048  h1de2bi  29331  spansni  29334  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  extdg1id  31053  ordtconnlem1  31167  cntnevol  31487  eulerpartgbij  31630  breprexpnat  31905  cvmlift2lem1  32549  cvmlift2lem12  32561  dfon2lem7  33034  bj-tagss  34295  lindsenlbs  34902  matunitlindflem1  34903  divrngidl  35321  isfldidl  35361  ispridlc  35363  pclfinclN  37101  osumcllem10N  37116  pexmidlem7N  37127  clsk1indlem4  40414  clsk1indlem1  40415  fourierdlem62  42473