Metamath Proof Explorer

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 ∈ V ↔ B ∈ V

Proof

Step Hyp Ref Expression
1 f1ofo ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ onto B
2 focdmex ⊢ A ∈ V → F : A ⟶ onto B → B ∈ V
3 1 2 syl5com ⊢ F : A ⟶ 1-1 onto B → A ∈ V → B ∈ V
4 f1of1 ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ 1-1 B
5 f1dmex ⊢ F : A ⟶ 1-1 B ∧ B ∈ V → A ∈ V
6 5 ex ⊢ F : A ⟶ 1-1 B → B ∈ V → A ∈ V
7 4 6 syl ⊢ F : A ⟶ 1-1 onto B → B ∈ V → A ∈ V
8 3 7 impbid ⊢ F : A ⟶ 1-1 onto B → A ∈ V ↔ B ∈ V