Theorem class2seteq

Description: Equality theorem based on 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		rabid2	|- ( A = { x e. A | A e. _V } <-> A. x e. A A e. _V )
5	3 4	sylibr	|- ( A e. _V -> A = { x e. A | A e. _V } )
6	5	eqcomd	|- ( A e. _V -> { x e. A | A e. _V } = A )
7	1 6	syl	|- ( A e. V -> { x e. A | A e. _V } = A )