Metamath Proof Explorer

Theorem isnumi

Description: A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	isnumi	$⊢ (A \in On \land A \approx B) \to B \in dom card$

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = A \to (x \approx B \leftrightarrow A \approx B)$
2	1	rspcev	$⊢ (A \in On \land A \approx B) \to \exists x \in On x \approx B$
3		isnum2	$⊢ B \in dom card \leftrightarrow \exists x \in On x \approx B$
4	2 3	sylibr	$⊢ (A \in On \land A \approx B) \to B \in dom card$