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 )