Theorem iunxsng

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016)

	Ref	Expression
Hypothesis	iunxsng.1	$$⊢x=A\to B=C$$
Assertion	iunxsng	$$⊢A\in V\to \bigcup _{x\in \left\{A\right\}}B=C$$

Proof

Step	Hyp	Ref	Expression
1		iunxsng.1	$$⊢x=A\to B=C$$
2		eliun	$$⊢y\in \bigcup _{x\in \left\{A\right\}}B\leftrightarrow \exists x\in \left\{A\right\}y\in B$$
3	1	eleq2d	$$⊢x=A\to \left(y\in B\leftrightarrow y\in C\right)$$
4	3	rexsng	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}y\in B\leftrightarrow y\in C\right)$$
5	2 4	bitrid	$$⊢A\in V\to \left(y\in \bigcup _{x\in \left\{A\right\}}B\leftrightarrow y\in C\right)$$
6	5	eqrdv	$$⊢A\in V\to \bigcup _{x\in \left\{A\right\}}B=C$$