This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )