f1ovv

Description: The 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 \underset{1-1 onto}{⟶} B \to (A \in V \leftrightarrow B \in V)$

Step	Hyp	Ref	Expression
1		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
2		fornex	$⊢ A \in V \to (F : A \underset{onto}{⟶} B \to B \in V)$
3	1 2	syl5com	$⊢ F : A \underset{1-1 onto}{⟶} B \to (A \in V \to B \in V)$
4		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
5		f1dmex	$⊢ (F : A \underset{1-1}{⟶} B \land B \in V) \to A \in V$
6	5	ex	$⊢ F : A \underset{1-1}{⟶} B \to (B \in V \to A \in V)$
7	4 6	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to (B \in V \to A \in V)$
8	3 7	impbid	$⊢ F : A \underset{1-1 onto}{⟶} B \to (A \in V \leftrightarrow B \in V)$

Metamath Proof Explorer