Theorem disjALTV0

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

	Ref	Expression
Assertion	disjALTV0	$$⊢Disj\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		br0	$$⊢\neg u\varnothing x$$
2	1	nex	$$⊢\neg \exists uu\varnothing x$$
3		nexmo	$$⊢\neg \exists uu\varnothing x\to {\exists }^{*}uu\varnothing x$$
4	2 3	ax-mp	$$⊢{\exists }^{*}uu\varnothing x$$
5	4	ax-gen	$$⊢\forall x{\exists }^{*}uu\varnothing x$$
6		rel0	$$⊢\mathrm{Rel}\varnothing$$
7		dfdisjALTV4	$$⊢Disj\varnothing \leftrightarrow \left(\forall x{\exists }^{*}uu\varnothing x\wedge \mathrm{Rel}\varnothing \right)$$
8	5 6 7	mpbir2an	$$⊢Disj\varnothing$$