Theorem fniinfv

Description: The indexed intersection of a function's values is the intersection of its range. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	fniinfv	⊢ ( 𝐹 Fn 𝐴 → ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
2	1	dfiin2	⊢ ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) }
3		fnrnfv	⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
4	3	inteqd	⊢ ( 𝐹 Fn 𝐴 → ∩ ran 𝐹 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
5	2 4	eqtr4id	⊢ ( 𝐹 Fn 𝐴 → ∩ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∩ ran 𝐹 )