disjALTV0

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

		Ref	Expression
	Assertion	disjALTV0	$⊢ Disj \emptyset$

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

Metamath Proof Explorer