Metamath Proof Explorer

Theorem bj-vjust

Description: Justification theorem for dfv2 if it were the definition. See also vjust . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-vjust	$⊢ \{x \| ⊤\} = \{y \| ⊤\}$

Proof

Step	Hyp	Ref	Expression
1		vextru	$⊢ z \in \{x \| ⊤\}$
2		vextru	$⊢ z \in \{y \| ⊤\}$
3	1 2	2th	$⊢ z \in \{x \| ⊤\} \leftrightarrow z \in \{y \| ⊤\}$
4	3	eqriv	$⊢ \{x \| ⊤\} = \{y \| ⊤\}$