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 2145  Vcvv 3451   ⊆ wss 3899  {csn 4584

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-sn 4585

This theorem is used by:  tpss  4797  sspwb  5417  nnullss  5430  exss  5431  pwssun  5543  fvimacnvi  7043  fvimacnv  7044  fvimacnvALT  7048  fnressn  7154  limensuci  9156  domunfican  9297  finsschain  9332  epfrs  9716  tc2  9725  tcsni  9726  dju1dif  10232  fpwwe2lem12  10708  wunfi  10787  uniwun  10806  un0mulcl  12621  nn0ssz  12697  xrinfmss  13421  hashbclem  14577  hashf1lem1  14580  hashf1lem2  14581  fsum2dlem  15916  fsumabs  15948  fsumrlim  15958  fsumo1  15959  fsumiun  15968  incexclem  15985  fprod2dlem  16127  lcmfunsnlem  16796  lcmfun  16800  coprmprod  16816  coprmproddvdslem  16817  ramcl2  17174  0ram  17178  strfv  17361  imasaddfnlem  17680  imasaddvallem  17681  acsfn1  17815  drsdirfi  18459  sylow2a  19813  gsumpt  20156  dprdfadd  20216  ablfac1eulem  20268  pgpfaclem1  20277  gsumle  20339  acsfn1p  21036  rsp1  21500  pzriprnglem4  21770  lindsenlbs  22137  mplcoe1  22326  mplcoe5  22329  mdetunilem9  22915  matunitlindflem1  22974  opnnei  23418  iscnp4  23561  cnpnei  23562  hausnei2  23651  fiuncmp  23702  llycmpkgen2  23849  1stckgen  23853  ptbasfi  23880  xkoccn  23918  xkoptsub  23953  ptcmpfi  24112  cnextcn  24366  tsmsid  24439  ustuqtop3  24542  utopreg  24551  prdsdsf  24666  prdsmet  24669  prdsbl  24790  fsumcn  25171  itgfsum  26127  dvmptfsum  26275  elply2  26494  elplyd  26500  ply1term  26502  ply0  26506  plymullem  26515  jensenlem1  27296  jensenlem2  27297  frcond3  30852  h1de2bi  32138  spansni  32141  gsumvsca1  33769  gsumvsca2  33770  1fldgenq  33866  unitprodclb  33926  mxidlirredi  33978  extdg1id  34280  ordtconnlem1  34538  cntnevol  34843  eulerpartgbij  34987  breprexpnat  35246  cvmlift2lem1  36036  cvmlift2lem12  36048  dfon2lem7  36521  axtco  37229  bj-tagss  37863  divrngidl  38930  isfldidl  38970  ispridlc  38972  pclfinclN  40975  osumcllem10N  40990  pexmidlem7N  41001  clsk1indlem4  45003  clsk1indlem1  45004  fourierdlem62  47122  numtowerdt  47860