Theorem vjust

Description: Justification theorem for df-v . (Contributed by Rodolfo Medina, 27-Apr-2010)

	Ref	Expression
Assertion	vjust	|- { x | x = x } = { y | y = y }

Proof

Step	Hyp	Ref	Expression
1		equid	|- x = x
2	1	vexw	|- z e. { x | x = x }
3		equid	|- y = y
4	3	vexw	|- z e. { y | y = y }
5	2 4	2th	|- ( z e. { x | x = x } <-> z e. { y | y = y } )
6	5	eqriv	|- { x | x = x } = { y | y = y }