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	⊢ ¬ 𝑢 ∅ 𝑥
2	1	nex	⊢ ¬ ∃ 𝑢 𝑢 ∅ 𝑥
3		nexmo	⊢ ( ¬ ∃ 𝑢 𝑢 ∅ 𝑥 → ∃* 𝑢 𝑢 ∅ 𝑥 )
4	2 3	ax-mp	⊢ ∃* 𝑢 𝑢 ∅ 𝑥
5	4	ax-gen	⊢ ∀ 𝑥 ∃* 𝑢 𝑢 ∅ 𝑥
6		rel0	⊢ Rel ∅
7		dfdisjALTV4	⊢ ( Disj ∅ ↔ ( ∀ 𝑥 ∃* 𝑢 𝑢 ∅ 𝑥 ∧ Rel ∅ ) )
8	5 6 7	mpbir2an	⊢ Disj ∅