Theorem f1dmex

Description: If the codomain of a one-to-one function exists, so does its domain. This theorem is equivalent to the Axiom of Replacement ax-rep . (Contributed by NM, 4-Sep-2004)

	Ref	Expression
Assertion	f1dmex	|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )

Proof

Step	Hyp	Ref	Expression
1		f1f	|- ( F : A -1-1-> B -> F : A --> B )
2	1	frnd	|- ( F : A -1-1-> B -> ran F C_ B )
3		ssexg	|- ( ( ran F C_ B /\ B e. C ) -> ran F e. _V )
4	2 3	sylan	|- ( ( F : A -1-1-> B /\ B e. C ) -> ran F e. _V )
5	4	ex	|- ( F : A -1-1-> B -> ( B e. C -> ran F e. _V ) )
6		f1cnv	|- ( F : A -1-1-> B -> `' F : ran F -1-1-onto-> A )
7		f1ofo	|- ( `' F : ran F -1-1-onto-> A -> `' F : ran F -onto-> A )
8	6 7	syl	|- ( F : A -1-1-> B -> `' F : ran F -onto-> A )
9		fornex	|- ( ran F e. _V -> ( `' F : ran F -onto-> A -> A e. _V ) )
10	5 8 9	syl6ci	|- ( F : A -1-1-> B -> ( B e. C -> A e. _V ) )
11	10	imp	|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )