Theorem prcnel

Description: A proper class doesn't belong to any class. (Contributed by Glauco Siliprandi, 17-Aug-2020) (Proof shortened by AV, 14-Nov-2020)

	Ref	Expression
Assertion	prcnel	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2	1	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ 𝑉 )