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 e. B -> U. { x e. B | x = A } = A )

Proof

Step	Hyp	Ref	Expression
1		rabsn	|- ( A e. B -> { x e. B | x = A } = { A } )
2	1	unieqd	|- ( A e. B -> U. { x e. B | x = A } = U. { A } )
3		unisng	|- ( A e. B -> U. { A } = A )
4	2 3	eqtrd	|- ( A e. B -> U. { x e. B | x = A } = A )