Theorem fniunfv

Description: The indexed union of a function's values is the union of its range. Compare Definition 5.4 of Monk1 p. 50. (Contributed by NM, 27-Sep-2004)

	Ref	Expression
Assertion	fniunfv	⊢ ( 𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ran 𝐹 )

Proof

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