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	$$⊢\phi \to A\in V$$
	iunsnima.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
Assertion	iunsnima	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\left[\left\{x\right\}\right]=B$$

Proof

Step	Hyp	Ref	Expression
1		iunsnima.1	$$⊢\phi \to A\in V$$
2		iunsnima.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	elimasn	$$⊢y\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\left[\left\{x\right\}\right]\leftrightarrow ⟨x,y⟩\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)$$
6		opeliunxp	$$⊢⟨x,y⟩\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\leftrightarrow \left(x\in A\wedge y\in B\right)$$
7	6	baib	$$⊢x\in A\to \left(⟨x,y⟩\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\leftrightarrow y\in B\right)$$
8	7	adantl	$$⊢\left(\phi \wedge x\in A\right)\to \left(⟨x,y⟩\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\leftrightarrow y\in B\right)$$
9	5 8	bitrid	$$⊢\left(\phi \wedge x\in A\right)\to \left(y\in \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\left[\left\{x\right\}\right]\leftrightarrow y\in B\right)$$
10	9	eqrdv	$$⊢\left(\phi \wedge x\in A\right)\to \bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\left[\left\{x\right\}\right]=B$$