Theorem eluniima

Description: Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Assertion	eluniima	⊢ ( Fun 𝐹 → ( 𝐵 ∈ ∪ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funiunfv	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ 𝐴 ) )
2	1	eleq2d	⊢ ( Fun 𝐹 → ( 𝐵 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 ∈ ∪ ( 𝐹 “ 𝐴 ) ) )
3		eliun	⊢ ( 𝐵 ∈ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) )
4	2 3	bitr3di	⊢ ( Fun 𝐹 → ( 𝐵 ∈ ∪ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ) )