Metamath Proof Explorer

Theorem enfi

Description: Equinumerous sets have the same finiteness. For a shorter proof using ax-pow , see enfiALT . (Contributed by NM, 22-Aug-2008) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)

		Ref	Expression
	Assertion	enfi	$⊢ A \approx B \to (A \in Fin \leftrightarrow B \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		ensymfib	$⊢ A \in Fin \to (A \approx B \leftrightarrow B \approx A)$
2	1	pm5.32i	$⊢ (A \in Fin \land A \approx B) \leftrightarrow (A \in Fin \land B \approx A)$
3		enfii	$⊢ (A \in Fin \land B \approx A) \to B \in Fin$
4	2 3	sylbi	$⊢ (A \in Fin \land A \approx B) \to B \in Fin$
5	4	expcom	$⊢ A \approx B \to (A \in Fin \to B \in Fin)$
6		enfii	$⊢ (B \in Fin \land A \approx B) \to A \in Fin$
7	6	expcom	$⊢ A \approx B \to (B \in Fin \to A \in Fin)$
8	5 7	impbid	$⊢ A \approx B \to (A \in Fin \leftrightarrow B \in Fin)$