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

Metamath Proof Explorer

Theorem iunsnima2

Description: Version of iunsnima with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 iunsnima.1 
 |-  ( ph -> A e. V )
2 iunsnima.2 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 iunsnima2.1 
 |-  F/_ x C
4 iunsnima2.2 
 |-  ( x = Y -> B = C )
5 elimasng 
 |-  ( ( Y e. A /\ z e. _V ) -> ( z e. ( U_ x e. A ( { x } X. B ) " { Y } ) <-> <. Y , z >. e. U_ x e. A ( { x } X. B ) ) )
6 5 elvd 
 |-  ( Y e. A -> ( z e. ( U_ x e. A ( { x } X. B ) " { Y } ) <-> <. Y , z >. e. U_ x e. A ( { x } X. B ) ) )
7 6 adantl 
 |-  ( ( ph /\ Y e. A ) -> ( z e. ( U_ x e. A ( { x } X. B ) " { Y } ) <-> <. Y , z >. e. U_ x e. A ( { x } X. B ) ) )
8 3 4 opeliunxp2f 
 |-  ( <. Y , z >. e. U_ x e. A ( { x } X. B ) <-> ( Y e. A /\ z e. C ) )
9 8 baib 
 |-  ( Y e. A -> ( <. Y , z >. e. U_ x e. A ( { x } X. B ) <-> z e. C ) )
10 9 adantl 
 |-  ( ( ph /\ Y e. A ) -> ( <. Y , z >. e. U_ x e. A ( { x } X. B ) <-> z e. C ) )
11 7 10 bitrd 
 |-  ( ( ph /\ Y e. A ) -> ( z e. ( U_ x e. A ( { x } X. B ) " { Y } ) <-> z e. C ) )
12 11 eqrdv 
 |-  ( ( ph /\ Y e. A ) -> ( U_ x e. A ( { x } X. B ) " { Y } ) = C )