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 = _V -> -. A e. B )

Proof

Step	Hyp	Ref	Expression
1		nvel	|- -. _V e. B
2		eleq1	|- ( _V = A -> ( _V e. B <-> A e. B ) )
3	2	eqcoms	|- ( A = _V -> ( _V e. B <-> A e. B ) )
4	1 3	mtbii	|- ( A = _V -> -. A e. B )