Metamath Proof Explorer


Theorem enfi

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

Ref Expression
Assertion enfi ( 𝐴𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 enen1 ( 𝐴𝐵 → ( 𝐴𝑥𝐵𝑥 ) )
2 1 rexbidv ( 𝐴𝐵 → ( ∃ 𝑥 ∈ ω 𝐴𝑥 ↔ ∃ 𝑥 ∈ ω 𝐵𝑥 ) )
3 isfi ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴𝑥 )
4 isfi ( 𝐵 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐵𝑥 )
5 2 3 4 3bitr4g ( 𝐴𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )