Metamath Proof Explorer

Theorem ennum

Description: Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion ennum ⊢ A ≈ B → A ∈ dom ⁡ card ↔ B ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 enen2 ⊢ A ≈ B → x ≈ A ↔ x ≈ B
2 1 rexbidv ⊢ A ≈ B → ∃ x ∈ On x ≈ A ↔ ∃ x ∈ On x ≈ B
3 isnum2 ⊢ A ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ A
4 isnum2 ⊢ B ∈ dom ⁡ card ↔ ∃ x ∈ On x ≈ B
5 2 3 4 3bitr4g ⊢ A ≈ B → A ∈ dom ⁡ card ↔ B ∈ dom ⁡ card