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

Metamath Proof Explorer

Theorem f1dm

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014) (Proof shortened by Wolf Lammen, 29-May-2024)

		Ref	Expression
	Assertion	f1dm	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$

Step	Hyp	Ref	Expression
1		f1fn	$⊢ F : A \underset{1-1}{⟶} B \to F Fn A$
2	1	fndmd	$⊢ F : A \underset{1-1}{⟶} B \to dom F = A$