Theorem dfv2

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

	Ref	Expression
Assertion	dfv2	$$⊢\mathrm{V}=\left\{x|\top \right\}$$

Proof

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