Theorem abfmpunirn

Description: Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016)

	Ref	Expression
Hypotheses	abfmpunirn.1	|- F = ( x e. V |-> { y | ph } )
	abfmpunirn.2	|- { y | ph } e. _V
	abfmpunirn.3	|- ( y = B -> ( ph <-> ps ) )
Assertion	abfmpunirn	|- ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ps ) )

Proof

Step	Hyp	Ref	Expression
1		abfmpunirn.1	|- F = ( x e. V |-> { y | ph } )
2		abfmpunirn.2	|- { y | ph } e. _V
3		abfmpunirn.3	|- ( y = B -> ( ph <-> ps ) )
4		elex	|- ( B e. U. ran F -> B e. _V )
5	2 1	fnmpti	|- F Fn V
6		fnunirn	|- ( F Fn V -> ( B e. U. ran F <-> E. x e. V B e. ( F ` x ) ) )
7	5 6	ax-mp	|- ( B e. U. ran F <-> E. x e. V B e. ( F ` x ) )
8	1	fvmpt2	|- ( ( x e. V /\ { y | ph } e. _V ) -> ( F ` x ) = { y | ph } )
9	2 8	mpan2	|- ( x e. V -> ( F ` x ) = { y | ph } )
10	9	eleq2d	|- ( x e. V -> ( B e. ( F ` x ) <-> B e. { y | ph } ) )
11	10	rexbiia	|- ( E. x e. V B e. ( F ` x ) <-> E. x e. V B e. { y | ph } )
12	7 11	bitri	|- ( B e. U. ran F <-> E. x e. V B e. { y | ph } )
13	3	elabg	|- ( B e. _V -> ( B e. { y | ph } <-> ps ) )
14	13	rexbidv	|- ( B e. _V -> ( E. x e. V B e. { y | ph } <-> E. x e. V ps ) )
15	12 14	bitrid	|- ( B e. _V -> ( B e. U. ran F <-> E. x e. V ps ) )
16	4 15	biadanii	|- ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ps ) )