Theorem enfiiOLD

Description: Obsolete version of enfii as of 23-Sep-2024. (Contributed by Mario Carneiro, 12-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	enfiiOLD	$$⊢\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}$$