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	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		f1ofo	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
2		focdmex	⊢ ( 𝐴 ∈ V → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )
3	1 2	syl5com	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V → 𝐵 ∈ V ) )
4		f1of1	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –1-1→ 𝐵 )
5		f1dmex	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
6	5	ex	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐵 ∈ V → 𝐴 ∈ V ) )
7	4 6	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐵 ∈ V → 𝐴 ∈ V ) )
8	3 7	impbid	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ V ↔ 𝐵 ∈ V ) )