Theorem rnfvprc

Description: The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022)

	Ref	Expression
Hypothesis	rnfvprc.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
Assertion	rnfvprc	⊢ ( ¬ 𝑋 ∈ V → ran 𝑌 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		rnfvprc.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
2		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
3	1 2	eqtrid	⊢ ( ¬ 𝑋 ∈ V → 𝑌 = ∅ )
4	3	rneqd	⊢ ( ¬ 𝑋 ∈ V → ran 𝑌 = ran ∅ )
5		rn0	⊢ ran ∅ = ∅
6	4 5	eqtrdi	⊢ ( ¬ 𝑋 ∈ V → ran 𝑌 = ∅ )