Theorem snss 4743

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-sn 4583

This theorem is referenced by:  tpss  4795  sspwb  5404  nnullss  5417  exss  5418  pwssun  5524  fvimacnvi  7006  fvimacnv  7007  fvimacnvALT  7011  fnressn  7113  limensuci  9093  domunfican  9234  finsschain  9271  epfrs  9652  tc2  9661  tcsni  9662  dju1dif  10095  fpwwe2lem12  10565  wunfi  10644  uniwun  10663  un0mulcl  12447  nn0ssz  12523  xrinfmss  13237  hashbclem  14387  hashf1lem1  14390  hashf1lem2  14391  fsum2dlem  15705  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  incexclem  15771  fprod2dlem  15915  lcmfunsnlem  16580  lcmfun  16584  coprmprod  16600  coprmproddvdslem  16601  ramcl2  16956  0ram  16960  strfv  17142  imasaddfnlem  17461  imasaddvallem  17462  acsfn1  17596  drsdirfi  18240  sylow2a  19560  gsumpt  19903  dprdfadd  19963  ablfac1eulem  20015  pgpfaclem1  20024  gsumle  20086  acsfn1p  20744  rsp1  21204  pzriprnglem4  21451  mplcoe1  22004  mplcoe5  22007  mdetunilem9  22576  opnnei  23076  iscnp4  23219  cnpnei  23220  hausnei2  23309  fiuncmp  23360  llycmpkgen2  23506  1stckgen  23510  ptbasfi  23537  xkoccn  23575  xkoptsub  23610  ptcmpfi  23769  cnextcn  24023  tsmsid  24096  ustuqtop3  24199  utopreg  24208  prdsdsf  24323  prdsmet  24326  prdsbl  24447  fsumcn  24829  itgfsum  25796  dvmptfsum  25947  elply2  26169  elplyd  26175  ply1term  26177  ply0  26181  plymullem  26189  jensenlem1  26965  jensenlem2  26966  frcond3  30356  h1de2bi  31641  spansni  31644  gsumvsca1  33319  gsumvsca2  33320  1fldgenq  33415  unitprodclb  33481  mxidlirredi  33563  extdg1id  33843  ordtconnlem1  34101  cntnevol  34405  eulerpartgbij  34549  breprexpnat  34811  cvmlift2lem1  35515  cvmlift2lem12  35527  dfon2lem7  36000  bj-tagss  37225  lindsenlbs  37863  matunitlindflem1  37864  divrngidl  38276  isfldidl  38316  ispridlc  38318  pclfinclN  40323  osumcllem10N  40338  pexmidlem7N  40349  clsk1indlem4  44397  clsk1indlem1  44398  fourierdlem62  46523  nthrucw  47241