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

Metamath Proof Explorer

Theorem foima

Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)

		Ref	Expression
	Assertion	foima	$⊢ F : A \underset{onto}{⟶} B \to F [A] = B$

Step	Hyp	Ref	Expression
1		imadmrn	$⊢ F [dom F] = ran F$
2		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
3	2	fdmd	$⊢ F : A \underset{onto}{⟶} B \to dom F = A$
4	3	imaeq2d	$⊢ F : A \underset{onto}{⟶} B \to F [dom F] = F [A]$
5		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
6	1 4 5	3eqtr3a	$⊢ F : A \underset{onto}{⟶} B \to F [A] = B$