Theorem fnrnafv

Description: The range of a function expressed as a collection of the function's values, analogous to fnrnfv . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	fnrnafv	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		dfafn5a	⊢ ( 𝐹 Fn 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) )
2	1	rneqd	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) )
4	3	rnmpt	⊢ ran ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ''' 𝑥 ) ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) }
5	2 4	eqtrdi	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ''' 𝑥 ) } )