Theorem class2seteq

Description: Writing a set as a class abstraction. This theorem looks artificial but was added to characterize the class abstraction whose existence is proved in class2set . (Contributed by NM, 13-Dec-2005) (Proof shortened by Raph Levien, 30-Jun-2006)

	Ref	Expression
Assertion	class2seteq	|- ( A e. V -> { x e. A | A e. _V } = A )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. V -> A e. _V )
2		ax-1	|- ( A e. _V -> ( x e. A -> A e. _V ) )
3	2	ralrimiv	|- ( A e. _V -> A. x e. A A e. _V )
4		rabid2im	|- ( A. x e. A A e. _V -> A = { x e. A | A e. _V } )
5	4	eqcomd	|- ( A. x e. A A e. _V -> { x e. A | A e. _V } = A )
6	1 3 5	3syl	|- ( A e. V -> { x e. A | A e. _V } = A )