Theorem f1ovv

Description: The codomain/range of a 1-1 onto function is a set iff its domain is a set. (Contributed by AV, 21-Mar-2019)

	Ref	Expression
Assertion	f1ovv	|- ( F : A -1-1-onto-> B -> ( A e. _V <-> B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		f1ofo	|- ( F : A -1-1-onto-> B -> F : A -onto-> B )
2		focdmex	|- ( A e. _V -> ( F : A -onto-> B -> B e. _V ) )
3	1 2	syl5com	|- ( F : A -1-1-onto-> B -> ( A e. _V -> B e. _V ) )
4		f1of1	|- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
5		f1dmex	|- ( ( F : A -1-1-> B /\ B e. _V ) -> A e. _V )
6	5	ex	|- ( F : A -1-1-> B -> ( B e. _V -> A e. _V ) )
7	4 6	syl	|- ( F : A -1-1-onto-> B -> ( B e. _V -> A e. _V ) )
8	3 7	impbid	|- ( F : A -1-1-onto-> B -> ( A e. _V <-> B e. _V ) )