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	⊢ ( 𝐴 = V → ¬ 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nvel	⊢ ¬ V ∈ 𝐵
2		eleq1	⊢ ( V = 𝐴 → ( V ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
3	2	eqcoms	⊢ ( 𝐴 = V → ( V ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
4	1 3	mtbii	⊢ ( 𝐴 = V → ¬ 𝐴 ∈ 𝐵 )