Theorem snss 4448

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

Syntax hints:   ↔ wb 196   ∈ wcel 2127  Vcvv 3328   ⊆ wss 3703  {csn 4309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-in 3710  df-ss 3717  df-sn 4310

This theorem is referenced by:  snssgOLD  4449  prssOLD  4485  tpss  4501  snelpw  5050  sspwb  5054  nnullss  5067  exss  5068  pwssun  5158  relsnOLD  5371  fvimacnvi  6482  fvimacnv  6483  fvimacnvALT  6487  fnressn  6576  limensuci  8289  domunfican  8386  finsschain  8426  epfrs  8768  tc2  8779  tcsni  8780  cda1dif  9161  fpwwe2lem13  9627  wunfi  9706  uniwun  9725  un0mulcl  11490  nn0ssz  11561  xrinfmss  12304  hashbclem  13399  hashf1lem1  13402  hashf1lem2  13403  fsum2dlem  14671  fsumabs  14703  fsumrlim  14713  fsumo1  14714  fsumiun  14723  incexclem  14738  fprod2dlem  14880  lcmfunsnlem  15527  lcmfun  15531  coprmprod  15548  coprmproddvdslem  15549  ramcl2  15893  0ram  15897  strfv  16080  imasaddfnlem  16361  imasaddvallem  16362  acsfn1  16494  drsdirfi  17110  sylow2a  18205  gsumpt  18532  dprdfadd  18590  ablfac1eulem  18642  pgpfaclem1  18651  rsp1  19397  mplcoe1  19638  mplcoe5  19641  mdetunilem9  20599  opnnei  21097  iscnp4  21240  cnpnei  21241  hausnei2  21330  fiuncmp  21380  llycmpkgen2  21526  1stckgen  21530  ptbasfi  21557  xkoccn  21595  xkoptsub  21630  ptcmpfi  21789  cnextcn  22043  tsmsid  22115  ustuqtop3  22219  utopreg  22228  prdsdsf  22344  prdsmet  22347  prdsbl  22468  fsumcn  22845  itgfsum  23763  dvmptfsum  23908  elply2  24122  elplyd  24128  ply1term  24130  ply0  24134  plymullem  24142  jensenlem1  24883  jensenlem2  24884  frcond3  27394  h1de2bi  28693  spansni  28696  gsumle  30059  gsumvsca1  30062  gsumvsca2  30063  ordtconnlem1  30250  cntnevol  30571  eulerpartgbij  30714  breprexpnat  30992  cvmlift2lem1  31562  cvmlift2lem12  31574  dfon2lem7  31970  bj-tagss  33245  lindsenlbs  33686  matunitlindflem1  33687  divrngidl  34109  isfldidl  34149  ispridlc  34151  pclfinclN  35708  osumcllem10N  35723  pexmidlem7N  35734  acsfn1p  38240  clsk1indlem4  38813  clsk1indlem1  38814  fourierdlem62  40857