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

Metamath Proof Explorer

Theorem dfv2

Description: Alternate definition of the universal class (see df-v ). (Contributed by BJ, 30-Nov-2019)

		Ref	Expression
	Assertion	dfv2	$⊢ V = \{x \| ⊤\}$

Step	Hyp	Ref	Expression
1		df-v	$⊢ V = \{x \| x = x\}$
2		equid	$⊢ x = x$
3	2	bitru	$⊢ x = x \leftrightarrow ⊤$
4	3	abbii	$⊢ \{x \| x = x\} = \{x \| ⊤\}$
5	1 4	eqtri	$⊢ V = \{x \| ⊤\}$