Theorem snssi 4746

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
snssi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 4744	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-sn 4585

This theorem is used by:  snssd  4747  difsnid  4771  eldifeldifsn  4772  pwpw0  4774  sssn  4787  ssunsn2  4788  tpssi  4798  frirr  5631  xpsspw  5790  djussxp  5825  dmressnsn  6016  fconst6g  6765  f1sng  6862  dffv2  6974  fvimacnvi  7045  fvimacnvALT  7050  fsn2  7131  fsnunf  7184  abnexg  7756  ordsuci  7808  curry1  8102  curry2  8105  xpord2pred  8144  xpord3pred  8151  ressuppss  8182  ressuppssdif  8184  naddcllem  8665  naddov2  8668  mapsnd  8894  ralxpmap  8904  fodomr  9127  findcard2  9160  findcard2s  9161  unfi  9166  ssfi  9168  sucdom2  9198  0sdom1dom  9217  enp1ilem  9249  fodomfir  9298  marypha1lem  9404  marypha2lem1  9406  epfrs  9711  dfac5lem4  10130  kmlem11  10164  ackbij1lem2  10223  fin23lem26  10328  isfin1-3  10389  hsmexlem4  10432  axdc3lem4  10456  axresscn  11158  nn0ssre  12533  nn0sscn  12534  xrsupss  13362  supxrmnf  13370  f1resfz0f1d  13849  1exp  14156  hashxrcl  14422  hashdifsn  14480  hashdifsnp1  14572  repsdf2  14850  modfsummods  15881  fsum00  15886  incexc  15927  2ebits  16538  bitsinvp1  16540  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  lcmfunsnlem2  16731  coprmproddvdslem  16753  4sqlem19  17056  ramxrcl  17110  mrcsncl  17701  acsfn1  17750  homaf  18120  dmcoass  18156  lubel  18603  gsumws1  18948  eqg0subgecsn  19326  cycsubg2  19339  cntzsnval  19452  0frgp  19907  dpjidcl  20188  ablfac1eu  20203  lspsncl  21162  lspsnss  21175  lspsnid  21178  rspsnid  21437  lpival  21556  lpiss  21561  lidldvgen  21566  pzriprnglem10  21704  znlidl  21747  frlmlbs  22011  lindsenlbs  22065  mat1dimelbas  22694  smadiadetglem2  22895  isneip  23331  neips  23339  opnneip  23345  maxlp  23373  restsn2  23397  leordtval2  23438  ist1-3  23575  ordtt1  23605  2ndcdisj2  23684  uffix  24148  neiflim  24201  ptcmplem5  24283  cnextfres1  24295  haustsms2  24364  ust0  24447  ustuqtop5  24472  dscopn  24800  icccmplem1  25050  bndth  25187  ovolsn  25724  icombl1  25792  plyun0  26423  coeeulem  26451  coeeu  26452  vieta1lem2  26544  aalioulem2  26570  taylfval  26596  perfectlem2  27467  noextend  27903  noextendseq  27904  conway  28045  etaslts  28059  0lt1s  28078  sltsleft  28126  sltsright  28127  negsid  28307  precsexlem8  28480  precsexlem11  28483  n0bday  28618  elreno2  28761  istrkg2ld  28802  axlowdimlem7  29406  axlowdimlem10  29409  0clwlkv  30602  hsn0elch  31730  chsupsn  31895  chsup0  32030  h1deoi  32031  h1dei  32032  h1did  32033  h1de2ctlem  32037  h1de2ci  32038  spansni  32039  spansnch  32042  elspansncl  32047  spansnpji  32060  spanunsni  32061  spanpr  32062  h1datomi  32063  spansnji  32128  h1da  32831  atom1d  32835  superpos  32836  disjun0  33069  djussxp2  33122  mptprop  33171  pwrssmgc  33441  gsumwrd2dccatlem  33518  elrgspnsubrunlem2  33689  1fldgenq  33764  lindssn  33812  elrspunidl  33857  esplyfval1  34084  esplyfvaln  34085  lbslsat  34127  fldextrspunlsplem  34184  esumnul  34559  esumcst  34574  hashf2  34595  esum2d  34604  measvuni  34726  cntnevol  34740  eulerpartlemt  34883  eulerpartlemmf  34887  eulerpartlemgh  34890  ballotlemfp1  35004  reprinfz1  35131  fineqvac  35643  dfon2lem3  36363  altxpsspw  36558  ttcmin  37116  ttcsnmin  37138  bj-snglss  37715  lindsadd  38368  poimirlem16  38386  poimirlem19  38389  poimirlem23  38393  poimirlem25  38395  poimirlem29  38399  poimirlem31  38401  mblfinlem2  38408  dvasin  38454  fdc  38496  prnc  38818  isfldidl  38819  ispridlc  38821  islshpsm  39854  snatpsubN  40624  polatN  40805  atpsubclN  40819  pclfinclN  40824  readvrec2  43237  mapfzcons  43562  mzpcompact2lem  43597  diophrw  43605  brfvidRP  44529  cotrcltrcl  44566  corcltrcl  44580  cotrclrcl  44583  gneispa  44971  binomcxplemnotnn0  45181  snelpwrVD  45654  disjiun2  45893  infxrpnf  46275  mccllem  46428  islptre  46450  cncfdmsn  46719  snmbl  46792  stoweidlem44  46873  sge0tsms  47209  sge0iunmptlemfi  47242  ismeannd  47296  isomenndlem  47359  hoidmvlelem3  47426  hoidmvlelem4  47427  ovnhoilem1  47430  fnbrafvb  48043  afvres  48061  afv2res  48128  perfectALTVlem2  48639  mapsnop  49275  lincext2  49386  snlindsntorlem  49401  resinsnALT  49800  aacllem  50773