Theorem snss 4739

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-sn 4580

This theorem is referenced by:  tpss  4791  sspwb  5396  nnullss  5409  exss  5410  pwssun  5515  fvimacnvi  6990  fvimacnv  6991  fvimacnvALT  6995  fnressn  7096  limensuci  9077  domunfican  9230  finsschain  9268  epfrs  9646  tc2  9657  tcsni  9658  dju1dif  10086  fpwwe2lem12  10555  wunfi  10634  uniwun  10653  un0mulcl  12436  nn0ssz  12512  xrinfmss  13230  hashbclem  14377  hashf1lem1  14380  hashf1lem2  14381  fsum2dlem  15695  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  incexclem  15761  fprod2dlem  15905  lcmfunsnlem  16570  lcmfun  16574  coprmprod  16590  coprmproddvdslem  16591  ramcl2  16946  0ram  16950  strfv  17132  imasaddfnlem  17450  imasaddvallem  17451  acsfn1  17585  drsdirfi  18229  sylow2a  19516  gsumpt  19859  dprdfadd  19919  ablfac1eulem  19971  pgpfaclem1  19980  gsumle  20042  acsfn1p  20702  rsp1  21162  pzriprnglem4  21409  mplcoe1  21960  mplcoe5  21963  mdetunilem9  22523  opnnei  23023  iscnp4  23166  cnpnei  23167  hausnei2  23256  fiuncmp  23307  llycmpkgen2  23453  1stckgen  23457  ptbasfi  23484  xkoccn  23522  xkoptsub  23557  ptcmpfi  23716  cnextcn  23970  tsmsid  24043  ustuqtop3  24147  utopreg  24156  prdsdsf  24271  prdsmet  24274  prdsbl  24395  fsumcn  24777  itgfsum  25744  dvmptfsum  25895  elply2  26117  elplyd  26123  ply1term  26125  ply0  26129  plymullem  26137  jensenlem1  26913  jensenlem2  26914  frcond3  30231  h1de2bi  31516  spansni  31519  gsumvsca1  33181  gsumvsca2  33182  1fldgenq  33274  unitprodclb  33339  mxidlirredi  33421  extdg1id  33640  ordtconnlem1  33893  cntnevol  34197  eulerpartgbij  34342  breprexpnat  34604  cvmlift2lem1  35277  cvmlift2lem12  35289  dfon2lem7  35765  bj-tagss  36956  lindsenlbs  37597  matunitlindflem1  37598  divrngidl  38010  isfldidl  38050  ispridlc  38052  pclfinclN  39932  osumcllem10N  39947  pexmidlem7N  39958  clsk1indlem4  44020  clsk1indlem1  44021  fourierdlem62  46153