Theorem snfig 7056

Description: A singleton is finite. For the proper class case, see snprc 3754. (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 6753	. . 3 |- 1o e. om
2		ensn1g 7037	. . 3 |- ( A e. V -> { A } ~~ 1o )
3		breq2 4113	. . . 4 |- ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )
4	3	rspcev 2921	. . 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 7000	. 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 2203   E.wrex 2521   {csn 3689   class class class wbr 4109   omcom 4712   1oc1o 6640   ~~ cen 6973   Fincfn 6975

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-1o 6647  df-en 6976  df-fin 6978

This theorem is referenced by:  fiprc  7057  ssfiexmid  7131  ssfiexmidt  7133  domfiexmid  7135  diffitest  7144  eqsndc  7163  unfiexmid  7178  prfidisj  7187  prfidceq  7188  tpfidisj  7189  mapfi  7214  snopfsuppdc  7252  ssfii  7261  infpwfidom  7501  hashsng  11161  fihashen1  11162  hashunsng  11172  hashprg  11173  hashdifsn  11184  hashdifpr  11185  hashxp  11191  hashmap  11192  hashfibclem  11206  hashtpgim  11217  fsumsplitsnun  12105  fsum2dlemstep  12120  fisumcom2  12124  fsumconst  12140  fsumge1  12147  fsum00  12148  hash2iun1dif1  12166  fprod2dlemstep  12308  fprodcom2fi  12312  fprodsplitsn  12319  fprodsplit1f  12320  phicl2  12911  lgsquadlem2  15951  1loopgrvd2fi  16300  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  p1evtxdeqfilem  16306  trlsegvdeglem7  16461  gfsumsn  16867