Theorem dfv2

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

	Ref	Expression
Assertion	dfv2	⊢ V = { 𝑥 ∣ ⊤ }

Proof

Step	Hyp	Ref	Expression
1		df-v	⊢ V = { 𝑥 ∣ 𝑥 = 𝑥 }
2		equid	⊢ 𝑥 = 𝑥
3	2	bitru	⊢ ( 𝑥 = 𝑥 ↔ ⊤ )
4	3	abbii	⊢ { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑥 ∣ ⊤ }
5	1 4	eqtri	⊢ V = { 𝑥 ∣ ⊤ }