Theorem snss 4740

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3902  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-sn 4580

This theorem is referenced by:  tpss  4792  sspwb  5413  nnullss  5426  exss  5427  pwssun  5535  fvimacnvi  7027  fvimacnv  7028  fvimacnvALT  7032  fnressn  7135  limensuci  9118  domunfican  9259  finsschain  9295  epfrs  9679  tc2  9688  tcsni  9689  dju1dif  10122  fpwwe2lem12  10593  wunfi  10672  uniwun  10691  un0mulcl  12508  nn0ssz  12584  xrinfmss  13306  hashbclem  14458  hashf1lem1  14461  hashf1lem2  14462  fsum2dlem  15787  fsumabs  15819  fsumrlim  15829  fsumo1  15830  fsumiun  15839  incexclem  15856  fprod2dlem  16000  lcmfunsnlem  16665  lcmfun  16669  coprmprod  16685  coprmproddvdslem  16686  ramcl2  17042  0ram  17046  strfv  17229  imasaddfnlem  17548  imasaddvallem  17549  acsfn1  17683  drsdirfi  18327  sylow2a  19649  gsumpt  19992  dprdfadd  20052  ablfac1eulem  20104  pgpfaclem1  20113  gsumle  20175  acsfn1p  20835  rsp1  21294  pzriprnglem4  21523  mplcoe1  22077  mplcoe5  22080  mdetunilem9  22667  opnnei  23167  iscnp4  23310  cnpnei  23311  hausnei2  23400  fiuncmp  23451  llycmpkgen2  23597  1stckgen  23601  ptbasfi  23628  xkoccn  23666  xkoptsub  23701  ptcmpfi  23860  cnextcn  24114  tsmsid  24187  ustuqtop3  24290  utopreg  24299  prdsdsf  24414  prdsmet  24417  prdsbl  24538  fsumcn  24919  itgfsum  25876  dvmptfsum  26024  elply2  26243  elplyd  26249  ply1term  26251  ply0  26255  plymullem  26263  jensenlem1  27038  jensenlem2  27039  frcond3  30427  h1de2bi  31713  spansni  31716  gsumvsca1  33366  gsumvsca2  33367  1fldgenq  33469  unitprodclb  33535  mxidlirredi  33619  extdg1id  33923  ordtconnlem1  34181  cntnevol  34485  eulerpartgbij  34629  breprexpnat  34888  cvmlift2lem1  35612  cvmlift2lem12  35624  dfon2lem7  36097  axtco  36791  bj-tagss  37425  lindsenlbs  38074  matunitlindflem1  38075  divrngidl  38487  isfldidl  38527  ispridlc  38529  pclfinclN  40534  osumcllem10N  40549  pexmidlem7N  40560  clsk1indlem4  44580  clsk1indlem1  44581  fourierdlem62  46702  nthrucw  47422