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 )