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 F /\ B e. ( F ` A ) ) -> B e. U. ran F )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	|- ( B e. ( F ` A ) -> A e. dom F )
2		fveq2	|- ( x = A -> ( F ` x ) = ( F ` A ) )
3	2	eleq2d	|- ( x = A -> ( B e. ( F ` x ) <-> B e. ( F ` A ) ) )
4	3	rspcev	|- ( ( A e. dom F /\ B e. ( F ` A ) ) -> E. x e. dom F B e. ( F ` x ) )
5	1 4	mpancom	|- ( B e. ( F ` A ) -> E. x e. dom F B e. ( F ` x ) )
6	5	adantl	|- ( ( Fun F /\ B e. ( F ` A ) ) -> E. x e. dom F B e. ( F ` x ) )
7		elunirn	|- ( Fun F -> ( B e. U. ran F <-> E. x e. dom F B e. ( F ` x ) ) )
8	7	adantr	|- ( ( Fun F /\ B e. ( F ` A ) ) -> ( B e. U. ran F <-> E. x e. dom F B e. ( F ` x ) ) )
9	6 8	mpbird	|- ( ( Fun F /\ B e. ( F ` A ) ) -> B e. U. ran F )