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

Metamath Proof Explorer

Theorem cardid

Description: Any set is equinumerous to its cardinal number. Proposition 10.5 of TakeutiZaring p. 85. (Contributed by NM, 22-Oct-2003) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypothesis cardval.1 ⊢ A ∈ V
Assertion cardid ⊢ card ⁡ A ≈ A

Proof

Step Hyp Ref Expression
1 cardval.1 ⊢ A ∈ V
2 numth3 ⊢ A ∈ V → A ∈ dom ⁡ card
3 cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A
4 1 2 3 mp2b ⊢ card ⁡ A ≈ A