Theorem snss 4751

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3906  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-sn 4591

This theorem is referenced by:  tpss  4803  sspwb  5432  nnullss  5445  exss  5446  pwssun  5555  fvimacnvi  7049  fvimacnv  7050  fvimacnvALT  7054  fnressn  7157  limensuci  9142  domunfican  9282  finsschain  9317  epfrs  9701  tc2  9710  tcsni  9711  dju1dif  10157  fpwwe2lem12  10628  wunfi  10707  uniwun  10726  un0mulcl  12539  nn0ssz  12615  xrinfmss  13337  hashbclem  14491  hashf1lem1  14494  hashf1lem2  14495  fsum2dlem  15823  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  incexclem  15892  fprod2dlem  16036  lcmfunsnlem  16700  lcmfun  16704  coprmprod  16720  coprmproddvdslem  16721  ramcl2  17077  0ram  17081  strfv  17264  imasaddfnlem  17583  imasaddvallem  17584  acsfn1  17718  drsdirfi  18362  sylow2a  19690  gsumpt  20033  dprdfadd  20093  ablfac1eulem  20145  pgpfaclem1  20154  gsumle  20216  acsfn1p  20883  rsp1  21347  pzriprnglem4  21615  mplcoe1  22169  mplcoe5  22172  mdetunilem9  22758  opnnei  23258  iscnp4  23401  cnpnei  23402  hausnei2  23491  fiuncmp  23542  llycmpkgen2  23688  1stckgen  23692  ptbasfi  23719  xkoccn  23757  xkoptsub  23792  ptcmpfi  23951  cnextcn  24205  tsmsid  24278  ustuqtop3  24381  utopreg  24390  prdsdsf  24505  prdsmet  24508  prdsbl  24629  fsumcn  25010  itgfsum  25967  dvmptfsum  26115  elply2  26334  elplyd  26340  ply1term  26342  ply0  26346  plymullem  26354  jensenlem1  27132  jensenlem2  27133  frcond3  30601  h1de2bi  31887  spansni  31890  gsumvsca1  33527  gsumvsca2  33528  1fldgenq  33624  unitprodclb  33683  mxidlirredi  33735  extdg1id  34037  ordtconnlem1  34295  cntnevol  34599  eulerpartgbij  34743  breprexpnat  35002  cvmlift2lem1  35775  cvmlift2lem12  35787  dfon2lem7  36260  axtco  36963  bj-tagss  37597  lindsenlbs  38247  matunitlindflem1  38248  divrngidl  38660  isfldidl  38700  ispridlc  38702  pclfinclN  40705  osumcllem10N  40720  pexmidlem7N  40731  clsk1indlem4  44753  clsk1indlem1  44754  fourierdlem62  46865  nthrucw  47590