Theorem unisn3

Description: Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008)

	Ref	Expression
Assertion	unisn3	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rabsn	⊢ ( 𝐴 ∈ 𝐵 → { 𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴 } = { 𝐴 } )
2	1	unieqd	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴 } = ∪ { 𝐴 } )
3		unisng	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝐴 } = 𝐴 )
4	2 3	eqtrd	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 = 𝐴 } = 𝐴 )