Theorem enfi

Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		enen1	$$⊢A\approx B\to \left(A\approx x\leftrightarrow B\approx x\right)$$
2	1	rexbidv	$$⊢A\approx B\to \left(\exists x\in \mathrm{\omega }A\approx x\leftrightarrow \exists x\in \mathrm{\omega }B\approx x\right)$$
3		isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
4		isfi	$$⊢B\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }B\approx x$$
5	2 3 4	3bitr4g	$$⊢A\approx B\to \left(A\in \mathrm{Fin}\leftrightarrow B\in \mathrm{Fin}\right)$$