# Metamath Proof Explorer

## Theorem snfi

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002)

Ref Expression
Assertion snfi
`|- { A } e. Fin`

### Proof

Step Hyp Ref Expression
1 1onn
` |-  1o e. _om`
2 ensn1g
` |-  ( A e. _V -> { A } ~~ 1o )`
3 breq2
` |-  ( x = 1o -> ( { A } ~~ x <-> { A } ~~ 1o ) )`
4 3 rspcev
` |-  ( ( 1o e. _om /\ { A } ~~ 1o ) -> E. x e. _om { A } ~~ x )`
5 1 2 4 sylancr
` |-  ( A e. _V -> E. x e. _om { A } ~~ x )`
6 snprc
` |-  ( -. A e. _V <-> { A } = (/) )`
7 en0
` |-  ( { A } ~~ (/) <-> { A } = (/) )`
8 peano1
` |-  (/) e. _om`
9 breq2
` |-  ( x = (/) -> ( { A } ~~ x <-> { A } ~~ (/) ) )`
10 9 rspcev
` |-  ( ( (/) e. _om /\ { A } ~~ (/) ) -> E. x e. _om { A } ~~ x )`
11 8 10 mpan
` |-  ( { A } ~~ (/) -> E. x e. _om { A } ~~ x )`
12 7 11 sylbir
` |-  ( { A } = (/) -> E. x e. _om { A } ~~ x )`
13 6 12 sylbi
` |-  ( -. A e. _V -> E. x e. _om { A } ~~ x )`
14 5 13 pm2.61i
` |-  E. x e. _om { A } ~~ x`
15 isfi
` |-  ( { A } e. Fin <-> E. x e. _om { A } ~~ x )`
16 14 15 mpbir
` |-  { A } e. Fin`