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	2	zfausab	|- { y | ( y e. W /\ ph ) } e. _V
8		eleq1	|- ( y = B -> ( y e. W <-> B e. W ) )
9	8 3	anbi12d	|- ( y = B -> ( ( y e. W /\ ph ) <-> ( B e. W /\ ps ) ) )
10	6 7 9	abfmpunirn	|- ( B e. U. ran F <-> ( B e. _V /\ E. x e. V ( B e. W /\ ps ) ) )
11		elex	|- ( B e. W -> B e. _V )
12	11	adantr	|- ( ( B e. W /\ ps ) -> B e. _V )
13	12	rexlimivw	|- ( E. x e. V ( B e. W /\ ps ) -> B e. _V )
14	13	pm4.71ri	|- ( E. x e. V ( B e. W /\ ps ) <-> ( B e. _V /\ E. x e. V ( B e. W /\ ps ) ) )
15	10 14	bitr4i	|- ( B e. U. ran F <-> E. x e. V ( B e. W /\ ps ) )