This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∅