Theorem vnex

Description: The universal class does not exist as a set. (Contributed by NM, 4-Jul-2005)

	Ref	Expression
Assertion	vnex	⊢ ¬ ∃ 𝑥 𝑥 = V

Proof

Step	Hyp	Ref	Expression
1		nalset	⊢ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥
2		vex	⊢ 𝑦 ∈ V
3	2	tbt	⊢ ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ V ) )
4	3	albii	⊢ ( ∀ 𝑦 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ V ) )
5		dfcleq	⊢ ( 𝑥 = V ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ V ) )
6	4 5	bitr4i	⊢ ( ∀ 𝑦 𝑦 ∈ 𝑥 ↔ 𝑥 = V )
7	6	exbii	⊢ ( ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 𝑥 = V )
8	1 7	mtbi	⊢ ¬ ∃ 𝑥 𝑥 = V