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	$$⊢A\in B\to \bigcup \left\{x\in B|x=A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		rabsn	$$⊢A\in B\to \left\{x\in B|x=A\right\}=\left\{A\right\}$$
2	1	unieqd	$$⊢A\in B\to \bigcup \left\{x\in B|x=A\right\}=\bigcup \left\{A\right\}$$
3		unisng	$$⊢A\in B\to \bigcup \left\{A\right\}=A$$
4	2 3	eqtrd	$$⊢A\in B\to \bigcup \left\{x\in B|x=A\right\}=A$$