Metamath Proof Explorer

Theorem 0fi

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008) Avoid ax-10 , ax-un . (Revised by BTernaryTau, 13-Jan-2025)

Ref Expression
Assertion 0fi 
|- (/) e. Fin

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 eqid 
 |-  (/) = (/)
3 en0 
 |-  ( (/) ~~ (/) <-> (/) = (/) )
4 2 3 mpbir 
 |-  (/) ~~ (/)
5 breq2 
 |-  ( x = (/) -> ( (/) ~~ x <-> (/) ~~ (/) ) )
6 5 rspcev 
 |-  ( ( (/) e. _om /\ (/) ~~ (/) ) -> E. x e. _om (/) ~~ x )
7 1 4 6 mp2an 
 |-  E. x e. _om (/) ~~ x
8 isfi 
 |-  ( (/) e. Fin <-> E. x e. _om (/) ~~ x )
9 7 8 mpbir 
 |-  (/) e. Fin