Theorem vjust

Description: Soundness 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	sbt	$$⊢\left[z/x\right]x=x$$
3		equid	$$⊢y=y$$
4	3	sbt	$$⊢\left[z/y\right]y=y$$
5	2 4	2th	$$⊢\left[z/x\right]x=x\leftrightarrow \left[z/y\right]y=y$$
6		df-clab	$$⊢z\in \left\{x|x=x\right\}\leftrightarrow \left[z/x\right]x=x$$
7		df-clab	$$⊢z\in \left\{y|y=y\right\}\leftrightarrow \left[z/y\right]y=y$$
8	5 6 7	3bitr4i	$$⊢z\in \left\{x|x=x\right\}\leftrightarrow z\in \left\{y|y=y\right\}$$
9	8	eqriv	$$⊢\left\{x|x=x\right\}=\left\{y|y=y\right\}$$