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

Metamath Proof Explorer

Theorem iunsnima

Description: Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020)

Ref Expression
Hypotheses iunsnima.1 
|- ( ph -> A e. V )
iunsnima.2 
|- ( ( ph /\ x e. A ) -> B e. W )
Assertion iunsnima 
|- ( ( ph /\ x e. A ) -> ( U_ x e. A ( { x } X. B ) " { x } ) = B )

Proof

Step Hyp Ref Expression
1 iunsnima.1 
 |-  ( ph -> A e. V )
2 iunsnima.2 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 elimasn 
 |-  ( y e. ( U_ x e. A ( { x } X. B ) " { x } ) <-> <. x , y >. e. U_ x e. A ( { x } X. B ) )
6 opeliunxp 
 |-  ( <. x , y >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ y e. B ) )
7 6 baib 
 |-  ( x e. A -> ( <. x , y >. e. U_ x e. A ( { x } X. B ) <-> y e. B ) )
8 7 adantl 
 |-  ( ( ph /\ x e. A ) -> ( <. x , y >. e. U_ x e. A ( { x } X. B ) <-> y e. B ) )
9 5 8 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( y e. ( U_ x e. A ( { x } X. B ) " { x } ) <-> y e. B ) )
10 9 eqrdv 
 |-  ( ( ph /\ x e. A ) -> ( U_ x e. A ( { x } X. B ) " { x } ) = B )