fundmeng

Description: A function is equinumerous to its domain. Exercise 4 of Suppes p. 98. (Contributed by NM, 17-Sep-2013)

		Ref	Expression
	Assertion	fundmeng	$⊢ (F \in V \land Fun F) \to dom F \approx F$

Step	Hyp	Ref	Expression
1		funeq	$⊢ x = F \to (Fun x \leftrightarrow Fun F)$
2		dmeq	$⊢ x = F \to dom x = dom F$
3		id	$⊢ x = F \to x = F$
4	2 3	breq12d	$⊢ x = F \to (dom x \approx x \leftrightarrow dom F \approx F)$
5	1 4	imbi12d	$⊢ x = F \to ((Fun x \to dom x \approx x) \leftrightarrow (Fun F \to dom F \approx F))$
6		vex	$⊢ x \in V$
7	6	fundmen	$⊢ Fun x \to dom x \approx x$
8	5 7	vtoclg	$⊢ F \in V \to (Fun F \to dom F \approx F)$
9	8	imp	$⊢ (F \in V \land Fun F) \to dom F \approx F$

Metamath Proof Explorer