Theorem snfig 6984

Description: A singleton is finite. For the proper class case, see snprc 3732. (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 6683	. . 3 |- 1o e. om
2		ensn1g 6966	. . 3 |- ( A e. V -> { A } ~~ 1o )
3		breq2 4090	. . . 4 |- ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )
4	3	rspcev 2908	. . 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 6929	. 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 2200   E.wrex 2509   {csn 3667   class class class wbr 4086   omcom 4686   1oc1o 6570   ~~ cen 6902   Fincfn 6904

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-nul 4213  ax-pow 4262  ax-pr 4297  ax-un 4528

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-br 4087  df-opab 4149  df-id 4388  df-suc 4466  df-iom 4687  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-1o 6577  df-en 6905  df-fin 6907

This theorem is referenced by:  fiprc  6985  ssfiexmid  7058  domfiexmid  7060  diffitest  7069  eqsndc  7088  unfiexmid  7103  prfidisj  7112  prfidceq  7113  tpfidisj  7114  ssfii  7164  infpwfidom  7399  hashsng  11050  fihashen1  11051  hashunsng  11061  hashprg  11062  hashdifsn  11073  hashdifpr  11074  hashxp  11080  fsumsplitsnun  11970  fsum2dlemstep  11985  fisumcom2  11989  fsumconst  12005  fsumge1  12012  fsum00  12013  hash2iun1dif1  12031  fprod2dlemstep  12173  fprodcom2fi  12177  fprodsplitsn  12184  fprodsplit1f  12185  phicl2  12776  lgsquadlem2  15797  1loopgrvd2fi  16111  1loopgrvd0fi  16112  1hevtxdg0fi  16113