Theorem snss 4593

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

Syntax hints:   ↔ wb 198   ∈ wcel 2050  Vcvv 3415   ⊆ wss 3831  {csn 4442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-in 3838  df-ss 3845  df-sn 4443

This theorem is referenced by:  tpss  4643  snelpw  5195  sspwb  5199  nnullss  5212  exss  5213  pwssun  5309  fvimacnvi  6649  fvimacnv  6650  fvimacnvALT  6654  fnressn  6745  limensuci  8491  domunfican  8588  finsschain  8628  epfrs  8969  tc2  8980  tcsni  8981  dju1dif  9398  fpwwe2lem13  9864  wunfi  9943  uniwun  9962  un0mulcl  11746  nn0ssz  11819  xrinfmss  12522  hashbclem  13626  hashf1lem1  13629  hashf1lem2  13630  fsum2dlem  14988  fsumabs  15019  fsumrlim  15029  fsumo1  15030  fsumiun  15039  incexclem  15054  fprod2dlem  15197  lcmfunsnlem  15844  lcmfun  15848  coprmprod  15864  coprmproddvdslem  15865  ramcl2  16211  0ram  16215  strfv  16390  imasaddfnlem  16660  imasaddvallem  16661  acsfn1  16793  drsdirfi  17409  sylow2a  18508  gsumpt  18838  dprdfadd  18895  ablfac1eulem  18947  pgpfaclem1  18956  acsfn1p  19303  rsp1  19721  mplcoe1  19962  mplcoe5  19965  mdetunilem9  20936  opnnei  21435  iscnp4  21578  cnpnei  21579  hausnei2  21668  fiuncmp  21719  llycmpkgen2  21865  1stckgen  21869  ptbasfi  21896  xkoccn  21934  xkoptsub  21969  ptcmpfi  22128  cnextcn  22382  tsmsid  22454  ustuqtop3  22558  utopreg  22567  prdsdsf  22683  prdsmet  22686  prdsbl  22807  fsumcn  23184  itgfsum  24133  dvmptfsum  24278  elply2  24492  elplyd  24498  ply1term  24500  ply0  24504  plymullem  24512  jensenlem1  25269  jensenlem2  25270  frcond3  27806  h1de2bi  29115  spansni  29118  gsumle  30522  gsumvsca1  30525  gsumvsca2  30526  extdg1id  30682  ordtconnlem1  30811  cntnevol  31132  eulerpartgbij  31275  breprexpnat  31553  cvmlift2lem1  32134  cvmlift2lem12  32146  dfon2lem7  32554  bj-tagss  33810  lindsenlbs  34328  matunitlindflem1  34329  divrngidl  34748  isfldidl  34788  ispridlc  34790  pclfinclN  36531  osumcllem10N  36546  pexmidlem7N  36557  clsk1indlem4  39757  clsk1indlem1  39758  fourierdlem62  41885