Theorem snss 4745

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-sn 4589

This theorem is used by:  tpss  4795  sspwb  5422  nnullss  5435  exss  5436  pwssun  5548  fvimacnvi  7077  fvimacnv  7078  fvimacnvALT  7082  fnressn  7189  limensuci  9203  domunfican  9344  finsschain  9379  epfrs  9762  tc2  9771  tcsni  9772  dju1dif  10281  fpwwe2lem12  10757  wunfi  10836  uniwun  10855  un0mulcl  12670  nn0ssz  12746  xrinfmss  13470  hashbclem  14627  hashf1lem1  14630  hashf1lem2  14631  fsum2dlem  15968  fsumabs  16000  fsumrlim  16010  fsumo1  16011  fsumiun  16020  incexclem  16037  fprod2dlem  16179  lcmfunsnlem  16848  lcmfun  16852  coprmprod  16868  coprmproddvdslem  16869  ramcl2  17226  0ram  17230  strfv  17413  imasaddfnlem  17732  imasaddvallem  17733  acsfn1  17867  drsdirfi  18511  sylow2a  19866  gsumpt  20209  dprdfadd  20269  ablfac1eulem  20321  pgpfaclem1  20330  gsumle  20392  acsfn1p  21089  rsp1  21553  pzriprnglem4  21823  lindsenlbs  22190  mplcoe1  22379  mplcoe5  22382  mdetunilem9  22968  matunitlindflem1  23027  opnnei  23471  iscnp4  23614  cnpnei  23615  hausnei2  23704  fiuncmp  23755  llycmpkgen2  23902  1stckgen  23906  ptbasfi  23933  xkoccn  23971  xkoptsub  24006  ptcmpfi  24165  cnextcn  24419  tsmsid  24492  ustuqtop3  24595  utopreg  24604  prdsdsf  24719  prdsmet  24722  prdsbl  24843  fsumcn  25224  itgfsum  26180  dvmptfsum  26328  elply2  26547  elplyd  26553  ply1term  26555  ply0  26559  plymullem  26568  jensenlem1  27347  jensenlem2  27348  frcond3  30903  h1de2bi  32189  spansni  32192  gsumvsca1  33863  gsumvsca2  33864  1fldgenq  33968  unitprodclb  34028  mxidlirredi  34080  extdg1id  34381  ordtconnlem1  34639  cntnevol  34944  eulerpartgbij  35087  breprexpnat  35346  cvmlift2lem1  36247  cvmlift2lem12  36259  dfon2lem7  36742  axtco  37450  bj-tagss  38084  divrngidl  39165  isfldidl  39205  ispridlc  39207  pclfinclN  41210  osumcllem10N  41225  pexmidlem7N  41236  clsk1indlem4  45247  clsk1indlem1  45248  fourierdlem62  47393  numtowerdt  48131