Theorem snssi 4745

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 4743	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 270	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3899  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-sn 4588

This theorem is used by:  snssd  4746  difsnid  4770  eldifeldifsn  4771  sssn  4784  ssunsn2  4785  tpssi  4795  pwpw0  4833  frirr  5630  xpsspw  5791  djussxp  5827  dmressnsn  6017  fconst6g  6779  f1sng  6876  dffv2  6988  fvimacnvi  7059  fvimacnvALT  7064  fsn2  7145  fsnunf  7197  abnexg  7777  ordsuci  7829  curry1  8125  curry2  8128  xpord2pred  8172  xpord3pred  8179  ressuppss  8211  ressuppssdif  8213  naddcllem  8696  naddov2  8699  mapsnd  8925  ralxpmap  8935  fodomr  9158  findcard2  9191  findcard2s  9192  unfi  9197  ssfi  9199  sucdom2  9229  0sdom1dom  9248  enp1ilem  9280  fodomfir  9330  marypha1lem  9435  marypha2lem1  9437  epfrs  9742  hfsn  9930  dfac5lem4  10215  kmlem11  10249  ackbij1lem2  10308  fin23lem26  10413  isfin1-3  10474  hsmexlem4  10517  axdc3lem4  10541  axresscn  11243  nn0ssre  12620  nn0sscn  12621  xrsupss  13449  supxrmnf  13457  f1resfz0f1d  13937  1exp  14244  hashxrcl  14511  hashdifsn  14569  hashdifsnp1  14661  repsdf2  14940  modfsummods  15972  fsum00  15977  incexc  16018  2ebits  16629  bitsinvp1  16631  lcmfunsnlem2lem1  16825  lcmfunsnlem2lem2  16826  lcmfunsnlem2  16827  coprmproddvdslem  16849  4sqlem19  17153  ramxrcl  17207  mrcsncl  17798  acsfn1  17847  homaf  18217  dmcoass  18253  lubel  18700  gsumws1  19046  eqg0subgecsn  19424  cycsubg2  19437  cntzsnval  19550  0frgp  20005  dpjidcl  20286  ablfac1eu  20301  lspsncl  21264  lspsnss  21277  lspsnid  21280  rspsnid  21539  lpival  21660  lpiss  21665  lidldvgen  21670  pzriprnglem10  21808  znlidl  21851  frlmlbs  22115  lindsenlbs  22169  mat1dimelbas  22798  smadiadetglem2  22999  isneip  23435  neips  23443  opnneip  23449  maxlp  23477  restsn2  23501  leordtval2  23542  ist1-3  23679  ordtt1  23709  2ndcdisj2  23788  uffix  24252  neiflim  24305  ptcmplem5  24387  cnextfres1  24399  haustsms2  24468  ust0  24551  ustuqtop5  24576  dscopn  24904  icccmplem1  25154  bndth  25291  ovolsn  25828  icombl1  25896  plyun0  26527  coeeulem  26555  coeeu  26556  vieta1lem2  26646  aalioulem2  26672  taylfval  26698  perfectlem2  27569  noextend  28035  noextendseq  28036  conway  28177  etaslts  28191  0lt1s  28210  sltsleft  28258  sltsright  28259  negsid  28439  precsexlem8  28612  precsexlem11  28615  n0bday  28750  elreno2  28893  istrkg2ld  28934  axlowdimlem7  29538  axlowdimlem10  29541  0clwlkv  30734  hsn0elch  31862  chsupsn  32027  chsup0  32162  h1deoi  32163  h1dei  32164  h1did  32165  h1de2ctlem  32169  h1de2ci  32170  spansni  32171  spansnch  32174  elspansncl  32179  spansnpji  32192  spanunsni  32193  spanpr  32194  h1datomi  32195  spansnji  32260  h1da  32963  atom1d  32967  superpos  32968  disjun0  33243  djussxp2  33296  mptprop  33345  pwrssmgc  33614  gsumwrd2dccatlem  33691  elrgspnsubrunlem2  33862  1fldgenq  33937  lindssn  33986  elrspunidl  34031  esplyfval1  34258  esplyfvaln  34259  lbslsat  34301  fldextrspunlsplem  34358  esumnul  34733  esumcst  34748  hashf2  34769  esum2d  34778  measvuni  34900  cntnevol  34914  eulerpartlemt  35056  eulerpartlemmf  35060  eulerpartlemgh  35063  ballotlemfp1  35177  reprinfz1  35304  fineqvac  35855  dfon2lem3  36674  altxpsspw  36869  ttcmin  37411  ttcsnmin  37433  bj-snglss  38010  lindsadd  38676  poimirlem16  38694  poimirlem19  38697  poimirlem23  38701  poimirlem25  38703  poimirlem29  38707  poimirlem31  38709  mblfinlem2  38716  dvasin  38762  negprop  38783  fdc  38819  prnc  39141  isfldidl  39142  ispridlc  39144  islshpsm  40177  snatpsubN  40947  polatN  41128  atpsubclN  41142  pclfinclN  41147  readvrec2  43552  mapfzcons  43867  mzpcompact2lem  43902  diophrw  43910  brfvidRP  44828  cotrcltrcl  44865  corcltrcl  44879  cotrclrcl  44882  gneispa  45270  binomcxplemnotnn0  45480  snelpwrVD  45952  disjiun2  46214  infxrpnf  46595  mccllem  46748  islptre  46770  cncfdmsn  47039  snmbl  47112  stoweidlem44  47193  sge0tsms  47529  sge0iunmptlemfi  47562  ismeannd  47616  isomenndlem  47679  hoidmvlelem3  47746  hoidmvlelem4  47747  ovnhoilem1  47750  fnbrafvb  48363  afvres  48381  afv2res  48448  perfectALTVlem2  48959  mapsnop  49595  lincext2  49706  snlindsntorlem  49721  resinsnALT  50125  aacllem  51153