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	|- ( F Fn I -> ( A e. U. ran F <-> E. x e. I A e. ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn I -> Fun F )
2		elunirn	|- ( Fun F -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )
3	1 2	syl	|- ( F Fn I -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )
4		fndm	|- ( F Fn I -> dom F = I )
5	4	rexeqdv	|- ( F Fn I -> ( E. x e. dom F A e. ( F ` x ) <-> E. x e. I A e. ( F ` x ) ) )
6	3 5	bitrd	|- ( F Fn I -> ( A e. U. ran F <-> E. x e. I A e. ( F ` x ) ) )