Theorem fnunirn

Description: Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	fnunirn	⊢ ( 𝐹 Fn 𝐼 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	⊢ ( 𝐹 Fn 𝐼 → Fun 𝐹 )
2		elunirn	⊢ ( Fun 𝐹 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
3	1 2	syl	⊢ ( 𝐹 Fn 𝐼 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
4		fndm	⊢ ( 𝐹 Fn 𝐼 → dom 𝐹 = 𝐼 )
5	4	rexeqdv	⊢ ( 𝐹 Fn 𝐼 → ( ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
6	3 5	bitrd	⊢ ( 𝐹 Fn 𝐼 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐼 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )