Theorem snfig 6905

Description: A singleton is finite. For the proper class case, see snprc 3697. (Contributed by Jim Kingdon, 13-Apr-2020.)

Assertion

Ref	Expression
snfig	|- ( A e. V -> { A } e. Fin )

Proof of Theorem snfig

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1onn 6605	. . 3 |- 1o e. om
2		ensn1g 6888	. . 3 |- ( A e. V -> { A } ~~ 1o )
3		breq2 4047	. . . 4 |- ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )
4	3	rspcev 2876	. . 3 |- ( ( 1o e. om /\ { A } ~~ 1o ) -> E. x e. om { A } ~~ x )
5	1, 2, 4	sylancr 414	. 2 |- ( A e. V -> E. x e. om { A } ~~ x )
6		isfi 6851	. 2 |- ( { A } e. Fin <-> E. x e. om { A } ~~ x )
7	5, 6	sylibr 134	1 |- ( A e. V -> { A } e. Fin )

Syntax hints:   -> wi 4   e. wcel 2175   E.wrex 2484   {csn 3632   class class class wbr 4043   omcom 4637   1oc1o 6494   ~~ cen 6824   Fincfn 6826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-nul 4169  ax-pow 4217  ax-pr 4252  ax-un 4479

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4339  df-suc 4417  df-iom 4638  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-fun 5272  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277  df-1o 6501  df-en 6827  df-fin 6829

This theorem is referenced by:  fiprc  6906  ssfiexmid  6972  domfiexmid  6974  diffitest  6983  unfiexmid  7014  prfidisj  7023  prfidceq  7024  tpfidisj  7025  ssfii  7075  infpwfidom  7305  hashsng  10941  fihashen1  10942  hashunsng  10950  hashprg  10951  hashdifsn  10962  hashdifpr  10963  hashxp  10969  fsumsplitsnun  11701  fsum2dlemstep  11716  fisumcom2  11720  fsumconst  11736  fsumge1  11743  fsum00  11744  hash2iun1dif1  11762  fprod2dlemstep  11904  fprodcom2fi  11908  fprodsplitsn  11915  fprodsplit1f  11916  phicl2  12507  lgsquadlem2  15526