Theorem vjust

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

	Ref	Expression
Assertion	vjust	$$⊢\left\{x|x=x\right\}=\left\{y|y=y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		equid	$$⊢x=x$$
2	1	vexw	$$⊢z\in \left\{x|x=x\right\}$$
3		equid	$$⊢y=y$$
4	3	vexw	$$⊢z\in \left\{y|y=y\right\}$$
5	2 4	2th	$$⊢z\in \left\{x|x=x\right\}\leftrightarrow z\in \left\{y|y=y\right\}$$
6	5	eqriv	$$⊢\left\{x|x=x\right\}=\left\{y|y=y\right\}$$