Theorem bj-df-v

Description: Alternate definition of the universal class. Actually, the current definition df-v should be proved from this one, and vex should be proved from this proposed definition together with vexw , which would remove from vex dependency on ax-13 (see also comment of vexw ). (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-df-v	$$⊢\mathrm{V}=\left\{x|\top \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢\mathrm{V}=\left\{x|\top \right\}\leftrightarrow \forall y\left(y\in \mathrm{V}\leftrightarrow y\in \left\{x|\top \right\}\right)$$
2		vex	$$⊢y\in \mathrm{V}$$
3		tru	$$⊢\top$$
4	3	vexw	$$⊢y\in \left\{x|\top \right\}$$
5	2 4	2th	$$⊢y\in \mathrm{V}\leftrightarrow y\in \left\{x|\top \right\}$$
6	1 5	mpgbir	$$⊢\mathrm{V}=\left\{x|\top \right\}$$