Theorem iunxsnf

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		iunxsnf.1	$$⊢\underset{\_}{Ⅎ}xC$$
2		iunxsnf.2	$$⊢A\in \mathrm{V}$$
3		iunxsnf.3	$$⊢x=A\to B=C$$
4	1 3	iunxsngf	$$⊢A\in \mathrm{V}\to \bigcup _{x\in \left\{A\right\}}B=C$$
5	2 4	ax-mp	$$⊢\bigcup _{x\in \left\{A\right\}}B=C$$