Metamath Proof Explorer

Theorem unipreima

Description: Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017)

Ref Expression
Assertion unipreima 
|- ( Fun F -> ( `' F " U. A ) = U_ x e. A ( `' F " x ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 r19.42v 
 |-  ( E. x e. A ( y e. dom F /\ ( F ` y ) e. x ) <-> ( y e. dom F /\ E. x e. A ( F ` y ) e. x ) )
3 2 bicomi 
 |-  ( ( y e. dom F /\ E. x e. A ( F ` y ) e. x ) <-> E. x e. A ( y e. dom F /\ ( F ` y ) e. x ) )
4 3 a1i 
 |-  ( F Fn dom F -> ( ( y e. dom F /\ E. x e. A ( F ` y ) e. x ) <-> E. x e. A ( y e. dom F /\ ( F ` y ) e. x ) ) )
5 eluni2 
 |-  ( ( F ` y ) e. U. A <-> E. x e. A ( F ` y ) e. x )
6 5 anbi2i 
 |-  ( ( y e. dom F /\ ( F ` y ) e. U. A ) <-> ( y e. dom F /\ E. x e. A ( F ` y ) e. x ) )
7 6 a1i 
 |-  ( F Fn dom F -> ( ( y e. dom F /\ ( F ` y ) e. U. A ) <-> ( y e. dom F /\ E. x e. A ( F ` y ) e. x ) ) )
8 elpreima 
 |-  ( F Fn dom F -> ( y e. ( `' F " x ) <-> ( y e. dom F /\ ( F ` y ) e. x ) ) )
9 8 rexbidv 
 |-  ( F Fn dom F -> ( E. x e. A y e. ( `' F " x ) <-> E. x e. A ( y e. dom F /\ ( F ` y ) e. x ) ) )
10 4 7 9 3bitr4d 
 |-  ( F Fn dom F -> ( ( y e. dom F /\ ( F ` y ) e. U. A ) <-> E. x e. A y e. ( `' F " x ) ) )
11 elpreima 
 |-  ( F Fn dom F -> ( y e. ( `' F " U. A ) <-> ( y e. dom F /\ ( F ` y ) e. U. A ) ) )
12 eliun 
 |-  ( y e. U_ x e. A ( `' F " x ) <-> E. x e. A y e. ( `' F " x ) )
13 12 a1i 
 |-  ( F Fn dom F -> ( y e. U_ x e. A ( `' F " x ) <-> E. x e. A y e. ( `' F " x ) ) )
14 10 11 13 3bitr4d 
 |-  ( F Fn dom F -> ( y e. ( `' F " U. A ) <-> y e. U_ x e. A ( `' F " x ) ) )
15 14 eqrdv 
 |-  ( F Fn dom F -> ( `' F " U. A ) = U_ x e. A ( `' F " x ) )
16 1 15 sylbi 
 |-  ( Fun F -> ( `' F " U. A ) = U_ x e. A ( `' F " x ) )