Theorem rabfmpunirn

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

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

Proof

Step	Hyp	Ref	Expression
1		rabfmpunirn.1	|- F = ( x e. V |-> { y e. W | ph } )
2		rabfmpunirn.2	|- W e. _V
3		rabfmpunirn.3	|- ( y = B -> ( ph <-> ps ) )
4		df-rab	|- { y e. W | ph } = { y | ( y e. W /\ ph ) }
5	4	mpteq2i	|- ( x e. V |-> { y e. W | ph } ) = ( x e. V |-> { y | ( y e. W /\ ph ) } )
6	1 5	eqtri	|- F = ( x e. V |-> { y | ( y e. W /\ ph ) } )
7		sepab	|- ( W e. _V -> { y | ( y e. W /\ ph ) } e. _V )
8	2 7	ax-mp	|- { y | ( y e. W /\ ph ) } e. _V
9		eleq1	|- ( y = B -> ( y e. W <-> B e. W ) )
10	9 3	anbi12d	|- ( y = B -> ( ( y e. W /\ ph ) <-> ( B e. W /\ ps ) ) )
11	6 8 10	abfmpunirn	|- ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ( B e. W /\ ps ) ) )
12		elex	|- ( B e. W -> B e. _V )
13	12	adantr	|- ( ( B e. W /\ ps ) -> B e. _V )
14	13	rexlimivw	|- ( E. x e. V ( B e. W /\ ps ) -> B e. _V )
15	14	pm4.71ri	|- ( E. x e. V ( B e. W /\ ps ) <-> ( B e. _V /\ E. x e. V ( B e. W /\ ps ) ) )
16	11 15	bitr4i	|- ( B e. U. ran F <-> E. x e. V ( B e. W /\ ps ) )