MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snfi Unicode version

Theorem snfi 7616
Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
snfi

Proof of Theorem snfi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 1onn 7307 . . . 4
2 ensn1g 7600 . . . 4
3 breq2 4456 . . . . 5
43rspcev 3210 . . . 4
51, 2, 4sylancr 663 . . 3
6 snprc 4093 . . . 4
7 en0 7598 . . . . 5
8 peano1 6719 . . . . . 6
9 breq2 4456 . . . . . . 7
109rspcev 3210 . . . . . 6
118, 10mpan 670 . . . . 5
127, 11sylbir 213 . . . 4
136, 12sylbi 195 . . 3
145, 13pm2.61i 164 . 2
15 isfi 7559 . 2
1614, 15mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  =wceq 1395  e.wcel 1818  E.wrex 2808   cvv 3109   c0 3784  {csn 4029   class class class wbr 4452   com 6700   c1o 7142   cen 7533   cfn 7536
This theorem is referenced by:  fiprc  7617  prfi  7815  tpfi  7816  fnfi  7818  unifpw  7843  snopfsupp  7872  sniffsupp  7889  ssfii  7899  cantnfp1lem1  8118  cantnfp1lem1OLD  8144  infpwfidom  8430  ackbij1lem4  8624  ackbij1lem9  8629  ackbij1lem10  8630  fin23lem21  8740  isfin1-3  8787  axcclem  8858  zornn0g  8906  hashsng  12438  hashen1  12439  hashunsng  12459  hashprg  12460  hashsnlei  12478  hashxplem  12491  hashmap  12493  hashfun  12495  hashbclem  12501  hashf1lem1  12504  hashf1lem2  12505  hashf1  12506  fsummsnunz  13569  fsumsplitsnun  13570  fsum2dlem  13585  fsumcom2  13589  ackbijnn  13640  incexclem  13648  isumltss  13660  fprod2dlem  13784  fprodcom2  13788  rexpen  13961  2ebits  14097  phicl2  14298  ramub1lem1  14544  cshwshashnsame  14588  acsfn1  15058  acsfiindd  15807  symg1hash  16420  odcau  16624  sylow2alem2  16638  gsumsnfd  16978  gsumzunsnd  16982  gsumunsnfd  16983  gsumpt  16988  gsumptOLD  16989  dprdfidOLD  17064  ablfac1eu  17124  pgpfaclem2  17133  ablfaclem3  17138  srgbinomlem4  17194  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvridlemOLD  18075  mplsubrg  18102  mvrcl  18111  mplmon  18125  mplmonmul  18126  mplcoe3OLD  18129  mplcoe2OLD  18133  psrbagsn  18160  psr1baslem  18224  funsnfsupOLD  18256  uvcff  18822  mat1dimelbas  18973  mat1dim0  18975  mat1dimid  18976  mat1dimmul  18978  mat1dimcrng  18979  mat1f1o  18980  mat1ghm  18985  mat1mhm  18986  mat1rhm  18987  mat1rngiso  18988  mat1scmat  19041  mvmumamul1  19056  mdetrsca  19105  mdetunilem9  19122  mdetmul  19125  pmatcoe1fsupp  19202  d1mat2pmat  19240  pmatcollpw3fi1lem1  19287  chpmat1dlem  19336  chpmat1d  19337  0cmp  19894  discmp  19898  bwth  19910  bwthOLD  19911  disllycmp  19999  dis1stc  20000  locfincmp  20027  dissnlocfin  20030  comppfsc  20033  1stckgenlem  20054  ptpjpre2  20081  ptopn2  20085  xkohaus  20154  xkoptsub  20155  ptcmpfi  20314  cfinufil  20429  ufinffr  20430  fin1aufil  20433  alexsubALTlem3  20549  ptcmplem5  20556  tmdgsum  20594  tsmsxplem1  20655  tsmsxplem2  20656  prdsmet  20873  imasdsf1olem  20876  prdsbl  20994  icccmplem1  21327  icccmplem2  21328  ovolsn  21906  ovolfiniun  21912  volfiniun  21957  i1f0  22094  fta1glem2  22567  fta1blem  22569  fta1lem  22703  vieta1lem2  22707  vieta1  22708  aalioulem2  22729  tayl0  22757  radcnv0  22811  wilthlem2  23343  fsumvma  23488  dchrfi  23530  cusgrafilem3  24481  eupath2lem3  24979  vdegp1ai  24984  vdegp1bi  24985  konigsberg  24987  usgreghash2spotv  25066  ffsrn  27552  locfinref  27844  esumcst  28071  esumsn  28072  hasheuni  28091  sibf0  28276  eulerpartlems  28299  eulerpartlemb  28307  ccatmulgnn0dir  28496  ofcccat  28498  plymulx0  28504  derangsn  28614  onsucsuccmpi  29908  finixpnum  30038  prdsbnd  30289  heiborlem3  30309  heiborlem8  30314  ismrer1  30334  reheibor  30335  elrfi  30626  mzpcompact2lem  30684  dfac11  31008  pwslnmlem0  31037  lpirlnr  31066  acsfn1p  31148  fsumsplitsn  31571  fprodsplitsn  31592  dvmptfprodlem  31741  dvnprodlem2  31744  stoweidlem44  31826  fourierdlem51  31940  fourierdlem80  31969  fouriersw  32014  fsummmodsnunz  32348  suppmptcfin  32972  lcosn0  33021  lincext2  33056  snlindsntor  33072  pclfinN  35624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-om 6701  df-1o 7149  df-en 7537  df-fin 7540
  Copyright terms: Public domain W3C validator