Theorem elunirn2

Description: Condition for the membership in the union of the range of a function. (Contributed by Thierry Arnoux, 13-Nov-2016)

	Ref	Expression
Assertion	elunirn2	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) → 𝐵 ∈ ∪ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → 𝐴 ∈ dom 𝐹 )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
3	2	eleq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) )
4	3	rspcev	⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) )
5	1 4	mpancom	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) )
6	5	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) )
7		elunirn	⊢ ( Fun 𝐹 → ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ) )
8	7	adantr	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) → ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ) )
9	6 8	mpbird	⊢ ( ( Fun 𝐹 ∧ 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) ) → 𝐵 ∈ ∪ ran 𝐹 )