Theorem snss 4746

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

Syntax hints:   ↔ wb 209   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-sn 4586

This theorem is referenced by:  tpss  4797  sspwb  5420  nnullss  5433  exss  5434  pwssun  5543  fvimacnvi  7037  fvimacnv  7038  fvimacnvALT  7042  fnressn  7145  limensuci  9129  domunfican  9269  finsschain  9304  epfrs  9688  tc2  9697  tcsni  9698  dju1dif  10144  fpwwe2lem12  10615  wunfi  10694  uniwun  10713  un0mulcl  12526  nn0ssz  12602  xrinfmss  13324  hashbclem  14477  hashf1lem1  14480  hashf1lem2  14481  fsum2dlem  15809  fsumabs  15841  fsumrlim  15851  fsumo1  15852  fsumiun  15861  incexclem  15878  fprod2dlem  16022  lcmfunsnlem  16687  lcmfun  16691  coprmprod  16707  coprmproddvdslem  16708  ramcl2  17064  0ram  17068  strfv  17251  imasaddfnlem  17570  imasaddvallem  17571  acsfn1  17705  drsdirfi  18349  sylow2a  19677  gsumpt  20020  dprdfadd  20080  ablfac1eulem  20132  pgpfaclem1  20141  gsumle  20203  acsfn1p  20868  rsp1  21332  pzriprnglem4  21591  mplcoe1  22145  mplcoe5  22148  mdetunilem9  22734  opnnei  23234  iscnp4  23377  cnpnei  23378  hausnei2  23467  fiuncmp  23518  llycmpkgen2  23664  1stckgen  23668  ptbasfi  23695  xkoccn  23733  xkoptsub  23768  ptcmpfi  23927  cnextcn  24181  tsmsid  24254  ustuqtop3  24357  utopreg  24366  prdsdsf  24481  prdsmet  24484  prdsbl  24605  fsumcn  24986  itgfsum  25943  dvmptfsum  26091  elply2  26310  elplyd  26316  ply1term  26318  ply0  26322  plymullem  26330  jensenlem1  27105  jensenlem2  27106  frcond3  30525  h1de2bi  31811  spansni  31814  gsumvsca1  33454  gsumvsca2  33455  1fldgenq  33553  unitprodclb  33613  mxidlirredi  33666  extdg1id  33968  ordtconnlem1  34226  cntnevol  34530  eulerpartgbij  34674  breprexpnat  34933  cvmlift2lem1  35660  cvmlift2lem12  35672  dfon2lem7  36145  axtco  36839  bj-tagss  37472  lindsenlbs  38121  matunitlindflem1  38122  divrngidl  38534  isfldidl  38574  ispridlc  38576  pclfinclN  40581  osumcllem10N  40596  pexmidlem7N  40607  clsk1indlem4  44627  clsk1indlem1  44628  fourierdlem62  46741  nthrucw  47461