Theorem enfii

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

	Ref	Expression
Assertion	enfii	$$⊢\left(B\in \mathrm{Fin}\wedge A\approx B\right)\to A\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		enfi	$$⊢A\approx B\to \left(A\in \mathrm{Fin}\leftrightarrow B\in \mathrm{Fin}\right)$$
2	1	biimparc	$$⊢\left(B\in \mathrm{Fin}\wedge A\approx B\right)\to A\in \mathrm{Fin}$$