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

Metamath Proof Explorer

Theorem fimacnv

Description: The preimage of the codomain of a function is the function's domain. (Contributed by FL, 25-Jan-2007) (Proof shortened by AV, 20-Sep-2024)

		Ref	Expression
	Assertion	fimacnv	$⊢ F : A ⟶ B \to F^{-1} [B] = A$

Proof

Step	Hyp	Ref	Expression
1		frn	$⊢ F : A ⟶ B \to ran F \subseteq B$
2		cnvimassrndm	$⊢ ran F \subseteq B \to F^{-1} [B] = dom F$
3	1 2	syl	$⊢ F : A ⟶ B \to F^{-1} [B] = dom F$
4		fdm	$⊢ F : A ⟶ B \to dom F = A$
5	3 4	eqtrd	$⊢ F : A ⟶ B \to F^{-1} [B] = A$