Theorem snssi 4812

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3945  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-ss 3962  df-sn 4630

This theorem is referenced by:  snssd  4813  difsnid  4814  eldifeldifsn  4815  pwpw0  4817  sssn  4830  ssunsn2  4831  tpssi  4840  snelpwiOLD  5445  intidOLD  5459  frirr  5654  xpsspw  5810  djussxp  5847  dmressnsn  6027  fconst6g  6784  f1sng  6878  dffv2  6990  fvimacnvi  7058  fvimacnvALT  7063  fsn2  7143  fsnunf  7192  abnexg  7757  ordsuci  7810  sucexeloniOLD  7812  suceloniOLD  7814  curry1  8107  curry2  8110  xpord2pred  8148  xpord3pred  8155  ressuppss  8186  ressuppssdif  8188  naddcllem  8695  naddov2  8698  mapsnd  8903  ralxpmap  8913  sucdom2OLD  9105  fodomr  9151  findcard2  9187  findcard2s  9188  unfi  9195  ssfi  9196  sucdom2  9229  0sdom1dom  9261  en1eqsnOLD  9298  enp1ilem  9301  findcard2OLD  9307  marypha1lem  9456  marypha2lem1  9458  epfrs  9754  dfac5lem4  10149  kmlem11  10183  ackbij1lem2  10244  fin23lem26  10348  isfin1-3  10409  hsmexlem4  10452  axdc3lem4  10476  axresscn  11171  nn0ssre  12506  nn0sscn  12507  xrsupss  13320  supxrmnf  13328  1exp  14088  hashxrcl  14348  hashdifsn  14405  hashdifsnp1  14489  repsdf2  14760  modfsummods  15771  fsum00  15776  incexc  15815  2ebits  16421  bitsinvp1  16423  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  coprmproddvdslem  16632  4sqlem19  16931  ramxrcl  16985  mrcsncl  17591  acsfn1  17640  homaf  18018  dmcoass  18054  lubel  18505  gsumws1  18794  eqg0subgecsn  19156  cycsubg2  19169  cntzsnval  19279  0frgp  19738  dpjidcl  20019  ablfac1eu  20034  lspsncl  20865  lspsnss  20878  lspsnid  20881  lpival  21218  lpiss  21223  lidldvgen  21228  pzriprnglem10  21420  znlidl  21467  frlmlbs  21735  mat1dimelbas  22403  smadiadetglem2  22604  isneip  23039  neips  23047  opnneip  23053  maxlp  23081  restsn2  23105  leordtval2  23146  ist1-3  23283  ordtt1  23313  2ndcdisj2  23391  uffix  23855  neiflim  23908  ptcmplem5  23990  cnextfres1  24002  haustsms2  24071  ust0  24154  ustuqtop5  24180  dscopn  24512  icccmplem1  24768  bndth  24914  ovolsn  25454  icombl1  25522  plyun0  26161  coeeulem  26188  coeeu  26189  vieta1lem2  26276  aalioulem2  26298  taylfval  26323  perfectlem2  27193  noextend  27629  noextendseq  27630  conway  27762  etasslt  27776  0slt1s  27792  ssltleft  27827  ssltright  27828  negsid  27983  precsexlem8  28146  precsexlem11  28149  n0sbday  28253  istrkg2ld  28320  axlowdimlem7  28815  axlowdimlem10  28818  0clwlkv  29997  hsn0elch  31114  chsupsn  31279  chsup0  31414  h1deoi  31415  h1dei  31416  h1did  31417  h1de2ctlem  31421  h1de2ci  31422  spansni  31423  spansnch  31426  elspansncl  31431  spansnpji  31444  spanunsni  31445  spanpr  31446  h1datomi  31447  spansnji  31512  h1da  32215  atom1d  32219  superpos  32220  disjun0  32442  djussxp2  32491  mptprop  32535  pwrssmgc  32784  1fldgenq  33069  rspsnid  33144  lindssn  33155  elrspunidl  33206  lbslsat  33384  esumnul  33737  esumcst  33752  hashf2  33773  esum2d  33782  measvuni  33903  cntnevol  33917  eulerpartlemt  34061  eulerpartlemmf  34065  eulerpartlemgh  34068  ballotlemfp1  34181  reprinfz1  34324  fineqvac  34787  f1resfz0f1d  34793  dfon2lem3  35451  altxpsspw  35643  bj-snglss  36519  lindsadd  37156  lindsenlbs  37158  poimirlem16  37179  poimirlem19  37182  poimirlem23  37186  poimirlem25  37188  poimirlem29  37192  poimirlem31  37194  mblfinlem2  37201  dvasin  37247  fdc  37288  prnc  37610  isfldidl  37611  ispridlc  37613  islshpsm  38521  snatpsubN  39292  polatN  39473  atpsubclN  39487  pclfinclN  39492  mapfzcons  42201  mzpcompact2lem  42236  diophrw  42244  brfvidRP  43183  cotrcltrcl  43220  corcltrcl  43234  cotrclrcl  43237  gneispa  43625  binomcxplemnotnn0  43858  snelpwrVD  44335  disjiun2  44487  infxrpnf  44891  mccllem  45048  islptre  45070  cncfdmsn  45341  snmbl  45414  stoweidlem44  45495  sge0tsms  45831  sge0iunmptlemfi  45864  ismeannd  45918  isomenndlem  45981  hoidmvlelem3  46048  hoidmvlelem4  46049  ovnhoilem1  46052  fnbrafvb  46597  afvres  46615  afv2res  46682  perfectALTVlem2  47125  mapsnop  47520  lincext2  47635  snlindsntorlem  47650  aacllem  48346

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »