bj-vjust

Description: Justification theorem for bj-df-v . See also vjust . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

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

Step	Hyp	Ref	Expression
1		df-clab	$⊢ z \in \{x \| ⊤\} \leftrightarrow [z/ x] ⊤$
2		sbv	$⊢ [z/ y] ⊤ \leftrightarrow ⊤$
3		df-clab	$⊢ z \in \{y \| ⊤\} \leftrightarrow [z/ y] ⊤$
4		sbv	$⊢ [z/ x] ⊤ \leftrightarrow ⊤$
5	2 3 4	3bitr4ri	$⊢ [z/ x] ⊤ \leftrightarrow z \in \{y \| ⊤\}$
6	1 5	bitri	$⊢ z \in \{x \| ⊤\} \leftrightarrow z \in \{y \| ⊤\}$
7	6	eqriv	$⊢ \{x \| ⊤\} = \{y \| ⊤\}$

Metamath Proof Explorer