Theorem nvelim

Description: If a class is the universal class it doesn't belong to any class, generalization of nvel . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	nvelim	$$⊢A=\mathrm{V}\to \neg A\in B$$

Proof

Step	Hyp	Ref	Expression
1		nvel	$$⊢\neg \mathrm{V}\in B$$
2		eleq1	$$⊢\mathrm{V}=A\to \left(\mathrm{V}\in B\leftrightarrow A\in B\right)$$
3	2	eqcoms	$$⊢A=\mathrm{V}\to \left(\mathrm{V}\in B\leftrightarrow A\in B\right)$$
4	1 3	mtbii	$$⊢A=\mathrm{V}\to \neg A\in B$$