Theorem f1ocnvdm

Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006)

	Ref	Expression
Assertion	f1ocnvdm	|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) e. A )

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
2		f1of	|- ( `' F : B -1-1-onto-> A -> `' F : B --> A )
3	1 2	syl	|- ( F : A -1-1-onto-> B -> `' F : B --> A )
4	3	ffvelcdmda	|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) e. A )