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

Metamath Proof Explorer

Theorem uni0

Description: The union of the empty set is the empty set. Theorem 8.7 of Quine p. 54. (Contributed by NM, 16-Sep-1993) Remove use of ax-nul . (Revised by Eric Schmidt, 4-Apr-2007) Avoid ax-11 . (Revised by TM, 1-Feb-2026)

		Ref	Expression
	Assertion	uni0	⊢ ∪ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑦 ∈ ∅
2	1	intnan	⊢ ¬ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅ )
3	2	nex	⊢ ¬ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅ )
4		eluni	⊢ ( 𝑥 ∈ ∪ ∅ ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ ∅ ) )
5	3 4	mtbir	⊢ ¬ 𝑥 ∈ ∪ ∅
6	5	nel0	⊢ ∪ ∅ = ∅