This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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\}$

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