Metamath Proof Explorer

Theorem enfii

Description: A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion enfii 
|- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )

Proof

Step Hyp Ref Expression
1 enfi 
 |-  ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
2 1 biimparc 
 |-  ( ( B e. Fin /\ A ~~ B ) -> A e. Fin )