fndmeng

Description: A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011)

		Ref	Expression
	Assertion	fndmeng	$⊢ (F Fn A \land A \in C) \to A \approx F$

Step	Hyp	Ref	Expression
1		fnex	$⊢ (F Fn A \land A \in C) \to F \in V$
2		fnfun	$⊢ F Fn A \to Fun F$
3	2	adantr	$⊢ (F Fn A \land A \in C) \to Fun F$
4		fundmeng	$⊢ (F \in V \land Fun F) \to dom F \approx F$
5	1 3 4	syl2anc	$⊢ (F Fn A \land A \in C) \to dom F \approx F$
6		fndm	$⊢ F Fn A \to dom F = A$
7	6	breq1d	$⊢ F Fn A \to (dom F \approx F \leftrightarrow A \approx F)$
8	7	adantr	$⊢ (F Fn A \land A \in C) \to (dom F \approx F \leftrightarrow A \approx F)$
9	5 8	mpbid	$⊢ (F Fn A \land A \in C) \to A \approx F$

Metamath Proof Explorer