This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hasheqf1o

Description: The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017)

Ref Expression
Assertion hasheqf1o ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ ∃ f f : A ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 hashen ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ A ≈ B
2 bren ⊢ A ≈ B ↔ ∃ f f : A ⟶ 1-1 onto B
3 1 2 bitrdi ⊢ A ∈ Fin ∧ B ∈ Fin → A = B ↔ ∃ f f : A ⟶ 1-1 onto B