Theorem nrelvOLD

Description: Obsolete version of nrelv as of 10-Jun-2026. (Contributed by Thierry Arnoux, 23-Jan-2022) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nrelvOLD	⊢ ¬ Rel V

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		0nelxp	⊢ ¬ ∅ ∈ ( V × V )
3		nelss	⊢ ( ( ∅ ∈ V ∧ ¬ ∅ ∈ ( V × V ) ) → ¬ V ⊆ ( V × V ) )
4	1 2 3	mp2an	⊢ ¬ V ⊆ ( V × V )
5		df-rel	⊢ ( Rel V ↔ V ⊆ ( V × V ) )
6	4 5	mtbir	⊢ ¬ Rel V