Theorem iunxsngf

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Mario Carneiro, 25-Jun-2016) (Revised by Thierry Arnoux, 2-May-2020) Avoid ax-13 . (Revised by Gino Giotto, 19-May-2023)

	Ref	Expression
Hypotheses	iunxsngf.1	$$⊢\underset{\_}{Ⅎ}xC$$
	iunxsngf.2	$$⊢x=A\to B=C$$
Assertion	iunxsngf	$$⊢A\in V\to \bigcup _{x\in \left\{A\right\}}B=C$$

Proof

Step	Hyp	Ref	Expression
1		iunxsngf.1	$$⊢\underset{\_}{Ⅎ}xC$$
2		iunxsngf.2	$$⊢x=A\to B=C$$
3		eliun	$$⊢y\in \bigcup _{x\in \left\{A\right\}}B\leftrightarrow \exists x\in \left\{A\right\}y\in B$$
4	1	nfcri	$$⊢Ⅎxy\in C$$
5	2	eleq2d	$$⊢x=A\to \left(y\in B\leftrightarrow y\in C\right)$$
6	4 5	rexsngf	$$⊢A\in V\to \left(\exists x\in \left\{A\right\}y\in B\leftrightarrow y\in C\right)$$
7	3 6	bitrid	$$⊢A\in V\to \left(y\in \bigcup _{x\in \left\{A\right\}}B\leftrightarrow y\in C\right)$$
8	7	eqrdv	$$⊢A\in V\to \bigcup _{x\in \left\{A\right\}}B=C$$