Theorem disjALTV0

Description: The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021)

	Ref	Expression
Assertion	disjALTV0	|- Disj (/)

Proof

Step	Hyp	Ref	Expression
1		br0	|- -. u (/) x
2	1	nex	|- -. E. u u (/) x
3		nexmo	|- ( -. E. u u (/) x -> E* u u (/) x )
4	2 3	ax-mp	|- E* u u (/) x
5	4	ax-gen	|- A. x E* u u (/) x
6		rel0	|- Rel (/)
7		dfdisjALTV4	|- ( Disj (/) <-> ( A. x E* u u (/) x /\ Rel (/) ) )
8	5 6 7	mpbir2an	|- Disj (/)