Description: A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | enfii | ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enfi | ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) ) | |
2 | 1 | biimparc | ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐴 ∈ Fin ) |