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	⊢ Ⅎ 𝑥 𝐶
	iunxsnf.2	⊢ 𝐴 ∈ V
	iunxsnf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion	iunxsnf	⊢ ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶

Proof

Step	Hyp	Ref	Expression
1		iunxsnf.1	⊢ Ⅎ 𝑥 𝐶
2		iunxsnf.2	⊢ 𝐴 ∈ V
3		iunxsnf.3	⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4	1 3	iunxsngf	⊢ ( 𝐴 ∈ V → ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶 )
5	2 4	ax-mp	⊢ ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶