Theorem snss 4810

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-sn 4649

This theorem is referenced by:  tpss  4862  sspwb  5469  nnullss  5482  exss  5483  pwssun  5590  fvimacnvi  7085  fvimacnv  7086  fvimacnvALT  7090  fnressn  7192  limensuci  9219  domunfican  9389  finsschain  9429  epfrs  9800  tc2  9811  tcsni  9812  dju1dif  10242  fpwwe2lem12  10711  wunfi  10790  uniwun  10809  un0mulcl  12587  nn0ssz  12662  xrinfmss  13372  hashbclem  14501  hashf1lem1  14504  hashf1lem2  14505  fsum2dlem  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  incexclem  15884  fprod2dlem  16028  lcmfunsnlem  16688  lcmfun  16692  coprmprod  16708  coprmproddvdslem  16709  ramcl2  17063  0ram  17067  strfv  17251  imasaddfnlem  17588  imasaddvallem  17589  acsfn1  17719  drsdirfi  18375  sylow2a  19661  gsumpt  20004  dprdfadd  20064  ablfac1eulem  20116  pgpfaclem1  20125  acsfn1p  20822  rsp1  21270  pzriprnglem4  21518  mplcoe1  22078  mplcoe5  22081  mdetunilem9  22647  opnnei  23149  iscnp4  23292  cnpnei  23293  hausnei2  23382  fiuncmp  23433  llycmpkgen2  23579  1stckgen  23583  ptbasfi  23610  xkoccn  23648  xkoptsub  23683  ptcmpfi  23842  cnextcn  24096  tsmsid  24169  ustuqtop3  24273  utopreg  24282  prdsdsf  24398  prdsmet  24401  prdsbl  24525  fsumcn  24913  itgfsum  25882  dvmptfsum  26033  elply2  26255  elplyd  26261  ply1term  26263  ply0  26267  plymullem  26275  jensenlem1  27048  jensenlem2  27049  frcond3  30301  h1de2bi  31586  spansni  31589  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  1fldgenq  33289  unitprodclb  33382  mxidlirredi  33464  extdg1id  33676  ordtconnlem1  33870  cntnevol  34192  eulerpartgbij  34337  breprexpnat  34611  cvmlift2lem1  35270  cvmlift2lem12  35282  dfon2lem7  35753  bj-tagss  36946  lindsenlbs  37575  matunitlindflem1  37576  divrngidl  37988  isfldidl  38028  ispridlc  38030  pclfinclN  39907  osumcllem10N  39922  pexmidlem7N  39933  clsk1indlem4  44006  clsk1indlem1  44007  fourierdlem62  46089